diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml
new file mode 100644
index 0000000..32457ed
--- /dev/null
+++ b/.github/workflows/bar.yml
@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+    # proposed in its pull request #2. Move both to a release tag once
+    # mission publishes one.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2
diff --git a/.gitignore b/.gitignore
index 01f8cdb..9a366ff 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,4 @@
 .lake/
+venv/
+scratch/
+__pycache__/
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..2cce051
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,90 @@
+/-
+  Command line front end for the MQTT packet codec.
+
+  One request per line, in the shape `op numbers`, where the op
+  and the numbers are parted by one space, and the numbers are
+  decimal numbers parted by commas, with no spaces inside the
+  number list. A line holds a number in plain decimal: no sign,
+  no leading zeros (the number 0 itself is written `0`), and at
+  most twenty digits. An empty line is passed over with no
+  answer. A request that breaks the line shape prints `error`.
+
+  The one operation:
+
+  - `parse` takes comma parted byte numbers and prints `ok:` and
+    the bytes of the packet printed back when the bytes are
+    exactly one packet this slice reads, and `none` when they
+    are not. The reprint is the packet read and written again,
+    byte for byte when the packet arrived in its printed form.
+    The full rules are in SPEC.md.
+-/
+
+import Mqtt
+
+open Mqtt
+
+/-- Read one number token: plain decimal digits, no sign, no
+    leading zeros but for the number 0 itself, at most twenty
+    digits. -/
+def parseNat (s : String) : Option Nat :=
+  let cs := s.toList
+  if cs.isEmpty ∨ 20 < cs.length then none
+  else if 1 < cs.length ∧ cs.head! = '0' then none
+  else if cs.all Char.isDigit then
+    some (cs.foldl (fun n c => n * 10 + (c.toNat - 48)) 0)
+  else none
+
+/-- Read the number list of a payload. The empty payload is the
+    empty list. -/
+def numsOf (payload : String) : Option (List Nat) :=
+  if payload.isEmpty then some []
+  else (payload.splitOn ",").mapM parseNat
+
+/-- Read the byte list of a payload: every number at most 255. -/
+def bytesOf (payload : String) : Option (List UInt8) :=
+  (numsOf payload).bind fun ns =>
+    if ns.all (· ≤ 255) then some (ns.map Nat.toUInt8) else none
+
+/-- Print a number list as comma parted decimal numbers. -/
+def joinNums (ns : List Nat) : String :=
+  ns.foldl (fun acc n => if acc.isEmpty then toString n else acc ++ "," ++ toString n) ""
+
+/-- Run one operation on one payload. The answer is `error` for a
+    malformed request, and `none` for well formed bytes that this
+    slice rejects. -/
+def run (op payload : String) : String :=
+  match op with
+  | "parse" =>
+    match bytesOf payload with
+    | none => "error"
+    | some bs =>
+      match parse bs with
+      | some v => "ok:" ++ joinNums ((print v).map UInt8.toNat)
+      | none => "none"
+  | _ => "error"
+
+/-- Answer one request line. An empty line gets no answer. -/
+def processLine (line : String) : Option String :=
+  if line.isEmpty then none
+  else
+    match line.splitOn " " with
+    | [op] => some (run op "")
+    | [op, payload] => some (run op payload)
+    | _ => some "error"
+
+/-- The line without its line ending: LF, or CR LF. -/
+def chomp (line : String) : String :=
+  let cs := line.toList
+  if cs.getLast? = some '\n' then
+    let cs := cs.dropLast
+    String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
+  else line
+
+def main : IO Unit := do
+  let stdin ← IO.getStdin
+  repeat
+    let line ← stdin.getLine
+    if line.isEmpty then break
+    match processLine (chomp line) with
+    | some out => IO.println out
+    | none => pure ()
diff --git a/Mqtt.lean b/Mqtt.lean
new file mode 100644
index 0000000..b802af6
--- /dev/null
+++ b/Mqtt.lean
@@ -0,0 +1,2 @@
+import Mqtt.Value
+import Mqtt.Parse
diff --git a/Mqtt/Parse.lean b/Mqtt/Parse.lean
new file mode 100644
index 0000000..628cc33
--- /dev/null
+++ b/Mqtt/Parse.lean
@@ -0,0 +1,370 @@
+/-
+  The MQTT 5.0 packet reader.
+
+  The reader works on a byte list and reads one packet from its
+  front, returning the packet and the bytes after it, so a
+  caller can walk a stream of packets arriving over TCP. It
+  never reads past the end of its input: every length in the
+  packet (the remaining length, a property length, a string or
+  binary length) is checked against the bytes that actually
+  remain before any of them are taken.
+
+  Rules the reader follows, beyond the layout in SPEC.md:
+
+  - A variable byte integer stops at four bytes: a continuation
+    bit on the fourth byte is rejected, and a value cut off by
+    the end of the input is rejected. An encoding that uses more
+    bytes than the value needs is accepted, as long as it fits
+    in four bytes (see SPEC.md for this pinned reading).
+  - A packet type outside the seven this slice covers is
+    rejected, and so is a fixed header flags nibble other than
+    the one the specification fixes for the type; PUBLISH is
+    the only type whose flags carry meaning, and its reserved
+    QoS value 3 is rejected.
+  - The body of a packet is cut out by its remaining length
+    first, and the type's reader must consume the cut exactly:
+    bytes left over inside the cut are rejected, and a field
+    that runs past the cut is rejected.
+  - Properties are checked against the specification's table:
+    an identifier with no table entry, an identifier not
+    allowed on the packet kind at hand, and a repeat of a single
+    use property are all rejected.
+-/
+
+import Mqtt.Value
+
+namespace Mqtt
+
+/-! ## Byte readers -/
+
+/-- Read a big endian number of exactly `k` bytes from the
+    front of a byte list. Returns the number and the bytes
+    after it, or `none` when fewer than `k` bytes stand there. -/
+def readNat : Nat → List UInt8 → Option (Nat × List UInt8)
+  | 0, bs => some (0, bs)
+  | _ + 1, [] => none
+  | k + 1, b :: bs =>
+    (readNat k bs).map fun (u, r) => (b.toNat * 256 ^ k + u, r)
+
+/-- The unfolding rule for `readNat` at a successor width on a
+    list with a head byte. -/
+theorem readNat_succ_cons (k : Nat) (b : UInt8) (bs : List UInt8) :
+    readNat (k + 1) (b :: bs) =
+      (readNat k bs).map fun (u, r) => (b.toNat * 256 ^ k + u, r) := by
+  rw [readNat]
+
+/-- Take `n` bytes off the front of a byte list, or `none` when
+    fewer than `n` bytes stand there. Returns the bytes taken
+    and the bytes after them. -/
+def readBytes (n : Nat) (bs : List UInt8) : Option (List UInt8 × List UInt8) :=
+  if bs.length ≥ n then some (bs.take n, bs.drop n) else none
+
+/-- Read one byte as a number. -/
+def readByte : List UInt8 → Option (Nat × List UInt8)
+  | [] => none
+  | b :: bs => some (b.toNat, bs)
+
+/-! ## The variable byte integer reader -/
+
+/-- Read a variable byte integer with at most `k` bytes left to
+    spend, accumulating `mult` times the groups still to come.
+    A byte below 128 ends the number. A continuation byte on
+    the last byte the count allows is rejected, and so is the
+    end of the input while a continuation bit stands. -/
+def decVBIGo (k acc mult : Nat) : List UInt8 → Option (Nat × List UInt8)
+  | [] => none
+  | b :: bs =>
+    if b.toNat < 128 then some (acc + mult * b.toNat, bs)
+    else if k ≤ 1 then none
+    else decVBIGo (k - 1) (acc + mult * (b.toNat - 128)) (mult * 128) bs
+
+/-- Read a variable byte integer (section 2.1.4): at most four
+    bytes. Returns the value and the bytes after it. -/
+def decVBI (bs : List UInt8) : Option (Nat × List UInt8) :=
+  decVBIGo 4 0 1 bs
+
+/-! ## String and binary readers -/
+
+/-- Check a decoded string field's characters: the strict
+    decoder has already settled well formedness; the null
+    character must also be absent (section 1.5.4). -/
+def checkChars (s : List Char) : Option (List Char) :=
+  if hasNul s then none else some s
+
+/-- Read a string field: the two byte length, that many bytes,
+    read as strict UTF-8 with no null character. -/
+def readStr (bs : List UInt8) : Option (List Char × List UInt8) := do
+  let (len, r1) ← readNat 2 bs
+  let (chunk, r2) ← readBytes len r1
+  let s ← (Utf8.decode chunk).bind checkChars
+  pure (s, r2)
+
+/-- Read a binary data field: the two byte length, then that
+    many bytes. -/
+def readBin (bs : List UInt8) : Option (List UInt8 × List UInt8) := do
+  let (len, r1) ← readNat 2 bs
+  readBytes len r1
+
+/-! ## Property readers -/
+
+/-- Read a property value of the given type. -/
+def readPropVal (t : PropType) : List UInt8 → Option (PropVal × List UInt8)
+  | bs =>
+    match t with
+    | .byte => (readNat 1 bs).map fun (n, r) => (.byte n, r)
+    | .twoByte => (readNat 2 bs).map fun (n, r) => (.twoByte n, r)
+    | .fourByte => (readNat 4 bs).map fun (n, r) => (.fourByte n, r)
+    | .varByte => (decVBI bs).map fun (n, r) => (.varByte n, r)
+    | .utf8 => (readStr bs).map fun (s, r) => (.utf8 s, r)
+    | .utf8Pair => do
+      let (k, r1) ← readStr bs
+      let (v, r2) ← readStr r1
+      pure (.utf8Pair k v, r2)
+    | .binary => (readBin bs).map fun (chunk, r) => (.binary chunk, r)
+
+/-- Read one property: the identifier as a variable byte
+    integer, checked against the table and the block's allowed
+    list, then the value in the shape of the table's type for
+    the identifier. A repeat of a single use property whose
+    identifier already stands in `seen` is rejected. -/
+def readEntry (s : PropSet) (seen : List Nat) (bs : List UInt8) :
+    Option (Property × List UInt8) := do
+  let (id, r1) ← decVBI bs
+  if (allowedOf s).contains id && (repeatableIn s id || !seen.contains id) then
+    match propTypeOf id with
+    | none => none
+    | some t => (readPropVal t r1).map fun (v, r2) => (⟨id, v⟩, r2)
+  else none
+
+/-- Read properties until the input runs out, or `none` when
+    one fails to read. The fuel is a bound on the number of
+    properties: each property takes at least two bytes (an
+    identifier and one value byte at the least), so the input
+    length is always fuel enough. The `seen` list carries the
+    identifiers already read in this block. -/
+def readEntriesGo : Nat → PropSet → List Nat → List UInt8 →
+    Option (List Property × List UInt8)
+  | 0, _, _, bs => if bs.isEmpty then some ([], bs) else none
+  | fuel + 1, s, seen, bs =>
+    if bs.isEmpty then some ([], bs)
+    else match readEntry s seen bs with
+      | none => none
+      | some (p, r1) =>
+        match readEntriesGo fuel s (p.id :: seen) r1 with
+        | none => none
+        | some (ps, r2) => some (p :: ps, r2)
+
+/-- Read a whole property block's insides: exactly the given
+    bytes, all consumed. -/
+def readEntries (s : PropSet) (seg : List UInt8) : Option (List Property) :=
+  match readEntriesGo seg.length s [] seg with
+  | some (ps, []) => some ps
+  | _ => none
+
+/-- Read a property block: the property length as a variable
+    byte integer, then exactly that many bytes of properties.
+    Bytes left over inside the block, or a block that runs past
+    the bytes at hand, are rejected. -/
+def readProps (s : PropSet) (bs : List UInt8) :
+    Option (List Property × List UInt8) := do
+  let (len, r1) ← decVBI bs
+  let (seg, r2) ← readBytes len r1
+  let ps ← readEntries s seg
+  pure (ps, r2)
+
+/-! ## SUBSCRIBE filter readers -/
+
+/-- Read a subscription options byte. The reserved bits 6 and
+    7 must be clear, and neither the QoS field nor the retain
+    handling field may hold the reserved value 3. -/
+def readOptsByte (b : Nat) : Option SubOpts :=
+  if b < 64 ∧ b % 4 ≠ 3 ∧ (b / 16) % 4 ≠ 3 then
+    some ⟨b % 4, (b / 4) % 2 = 1, (b / 8) % 2 = 1, (b / 16) % 4⟩
+  else none
+
+/-- Read topic filters until the input runs out, or `none`
+    when one fails to read. The fuel is a bound on the number
+    of filters: each filter takes at least three bytes (a two
+    byte length and an options byte), so the input length is
+    always fuel enough. -/
+def readFiltersGo : Nat → List UInt8 →
+    Option (List (List Char × SubOpts) × List UInt8)
+  | 0, bs => if bs.isEmpty then some ([], bs) else none
+  | fuel + 1, bs =>
+    if bs.isEmpty then some ([], bs)
+    else match readStr bs with
+      | none => none
+      | some (f, ob :: r2) =>
+        match readOptsByte ob.toNat with
+        | none => none
+        | some o =>
+          match readFiltersGo fuel r2 with
+          | none => none
+          | some (fs, r3) => some ((f, o) :: fs, r3)
+      | some (_, []) => none
+
+/-! ## Body readers -/
+
+/-- The `k`th bit of a number, as a boolean: bit 0 is the least
+    significant. -/
+def flagBit (n k : Nat) : Bool := (n / 2 ^ k) % 2 = 1
+
+/-- A topic name check for a read string: not empty, and
+    neither wildcard character stands in it. -/
+def checkTopic (s : List Char) : Option (List Char) :=
+  if s.isEmpty || s.any (fun c => decide (c = '+')) || s.any (fun c => decide (c = '#')) then
+    none
+  else some s
+
+/-- Read the will step of a CONNECT body: the will
+    properties, will topic and will payload when the will
+    flag is set, nothing when it is clear. The will QoS and
+    will retain come from the connect flags byte. -/
+def readWillPart (flags : Nat) (r6 : List UInt8) :
+    Option (Option Will × List UInt8) :=
+  if flagBit flags 2 then
+    (readProps .will r6).bind fun (wprops, s1) =>
+    (readStr s1).bind fun (wtopic, s2) =>
+    (checkTopic wtopic).bind fun wtopic =>
+    (readBin s2).bind fun (wpay, s3) =>
+    some (some ⟨(flags / 8) % 4, flagBit flags 5, wprops, wtopic, wpay⟩, s3)
+  else some (none, r6)
+
+/-- Read an optional string field of a CONNECT payload,
+    present exactly when its connect flag bit is set. -/
+def readOptStrField (cond : Bool) (r : List UInt8) :
+    Option (Option (List Char) × List UInt8) :=
+  if cond then (readStr r).map fun (u, r') => (some u, r')
+  else some (none, r)
+
+/-- Read an optional binary field of a CONNECT payload,
+    present exactly when its connect flag bit is set. -/
+def readOptBinField (cond : Bool) (r : List UInt8) :
+    Option (Option (List UInt8) × List UInt8) :=
+  if cond then (readBin r).map fun (p, r') => (some p, r')
+  else some (none, r)
+
+/-- Read a CONNECT body: the whole body cut, nothing left
+    over. The protocol name must be "MQTT" and the level 5. The
+    reserved connect flag bit must be clear and the will QoS
+    must not be the reserved value 3. The payload fields stand
+    exactly when the connect flags say they stand. -/
+def readConnectBody (seg : List UInt8) : Option Connect :=
+  (readStr seg).bind fun (proto, r1) =>
+  if proto = ['M', 'Q', 'T', 'T'] then
+    (readByte r1).bind fun (level, r2) =>
+    if level = 5 then
+      (readByte r2).bind fun (flags, r3) =>
+      if flags % 2 = 0 then
+      if (flags / 8) % 4 ≠ 3 then
+        (readNat 2 r3).bind fun (ka, r4) =>
+        (readProps .connect r4).bind fun (props, r5) =>
+        (readStr r5).bind fun (cid, r6) =>
+        (readWillPart flags r6).bind fun (will, r7) =>
+        (readOptStrField (flagBit flags 7) r7).bind fun (username, r8) =>
+        (readOptBinField (flagBit flags 6) r8).bind fun (password, r9) =>
+        if r9.isEmpty then
+          some ⟨flagBit flags 1, ka, props, cid, will, username, password⟩
+        else none
+      else none
+      else none
+    else none
+  else none
+
+/-- Read the packet identifier step of a PUBLISH body: no
+    identifier at QoS 0, a two byte nonzero identifier at
+    QoS 1 and 2. -/
+def readPacketId (flags : Nat) (r1 : List UInt8) :
+    Option (Option Nat × List UInt8) :=
+  if (flags / 2) % 4 = 0 then some (none, r1)
+  else (readNat 2 r1).bind fun (id, r) =>
+    if id ≠ 0 then some (some id, r) else none
+
+/-- Read a PUBLISH body: topic name, the packet identifier
+    when the QoS is 1 or 2 (and never 0), the properties, and
+    the payload, which is all the bytes that remain in the cut.
+    The QoS comes from the fixed header flags; the reserved
+    value 3 has already been turned away by the caller. -/
+def readPublishBody (flags : Nat) (seg : List UInt8) : Option Publish :=
+  (readStr seg).bind fun (topic, r1) =>
+  (checkTopic topic).bind fun topic =>
+  (readPacketId flags r1).bind fun (pid, r2) =>
+  (readProps .publish r2).bind fun (props, payload) =>
+  some ⟨flagBit flags 3, (flags / 2) % 4, flagBit flags 0, topic, pid,
+    props, payload⟩
+
+/-- Read a SUBSCRIBE body: a nonzero packet identifier, the
+    properties, and a nonempty list of topic filters that
+    fills the rest of the cut exactly. -/
+def readSubscribeBody (seg : List UInt8) : Option Packet := do
+  let (id, r1) ← readNat 2 seg
+  if id ≠ 0 then pure () else none
+  let (props, r2) ← readProps .subscribe r1
+  let (fs, r3) ← readFiltersGo r2.length r2
+  if r3.isEmpty && !fs.isEmpty then pure (.subscribe id props fs) else none
+
+/-- Read a SUBACK body: a nonzero packet identifier, the
+    properties, and a nonempty list of reason codes filling
+    the rest of the cut. -/
+def readSubackBody (seg : List UInt8) : Option Packet := do
+  let (id, r1) ← readNat 2 seg
+  if id ≠ 0 then pure () else none
+  let (props, r2) ← readProps .suback r1
+  if !r2.isEmpty then pure (.suback id props (r2.map UInt8.toNat)) else none
+
+/-- Read a DISCONNECT body: an empty cut is a normal
+    disconnection with no body. A cut of one byte is a reason
+    code on its own: the specification omits the property
+    length when the remaining length is 1 (section 3.14.2).
+    A longer cut is a reason code and a property block that
+    fills the rest of the cut. -/
+def readDisconnectBody (seg : List UInt8) : Option Packet :=
+  match seg with
+  | [] => some (.disconnect none)
+  | rc :: r1 =>
+    if r1.isEmpty then some (.disconnect (some (rc.toNat, [])))
+    else do
+      let (props, r2) ← readProps .disconnect r1
+      if r2.isEmpty then pure (.disconnect (some (rc.toNat, props))) else none
+
+/-- Read a packet body of the given type, with the given fixed
+    header flags, from a body cut out by the remaining length.
+    The reader must consume the cut exactly. Packet types
+    outside the seven this slice covers are rejected, and so
+    is a flags nibble other than the one the specification
+    fixes for the type. -/
+def parseBody (typ flags : Nat) (seg : List UInt8) : Option Packet :=
+  match typ with
+  | 1 => if flags = 0 then (readConnectBody seg).map Packet.connect else none
+  | 3 =>
+    if (flags / 2) % 4 = 3 then none
+    else (readPublishBody flags seg).map Packet.publish
+  | 8 => if flags = 2 then readSubscribeBody seg else none
+  | 9 => if flags = 0 then readSubackBody seg else none
+  | 12 => if flags = 0 && seg.isEmpty then some .pingreq else none
+  | 13 => if flags = 0 && seg.isEmpty then some .pingresp else none
+  | 14 => if flags = 0 then readDisconnectBody seg else none
+  | _ => none
+
+/-! ## The packet reader -/
+
+/-- Read one packet from the front of a byte list: the fixed
+    header byte, the remaining length, and exactly that many
+    body bytes. Returns the packet and the bytes after it. -/
+def parsePacket (bs : List UInt8) : Option (Packet × List UInt8) :=
+  match bs with
+  | [] => none
+  | b :: r0 => do
+    let (len, r1) ← decVBI r0
+    let (seg, r2) ← readBytes len r1
+    let p ← parseBody (b.toNat / 16) (b.toNat % 16) seg
+    pure (p, r2)
+
+/-- Read one whole packet: exactly one packet, with nothing
+    after it. -/
+def parse (bs : List UInt8) : Option Packet :=
+  match parsePacket bs with
+  | some (p, []) => some p
+  | _ => none
+
+end Mqtt
diff --git a/Mqtt/Utf8.lean b/Mqtt/Utf8.lean
new file mode 100644
index 0000000..05ca366
--- /dev/null
+++ b/Mqtt/Utf8.lean
@@ -0,0 +1,85 @@
+/-
+  UTF-8, by hand: MQTT strings travel on the wire as bytes, and
+  the string fields in this slice are held as lists of
+  characters, so the packet code needs both directions between
+  characters and bytes.
+
+  The encoder writes the standard one to four bytes per
+  character. The decoder is strict. It turns away stray
+  continuation bytes, overlong forms (a character written with
+  more bytes than it needs, including any lead byte below C2),
+  lead bytes above F4, encodings of the surrogate values D800 to
+  DFFF, values above 10FFFF, and truncated sequences.
+
+  This file is carried in from the jws project's Jws/Utf8.lean,
+  written for the Proven Commons jws slice, with the namespace
+  renamed. The repos in this programme do not share a library,
+  so the code travels.
+-/
+
+namespace Mqtt.Utf8
+
+/-- The bytes of one character. -/
+def encodeChar (c : Char) : List UInt8 :=
+  let n := c.toNat
+  if n < 0x80 then [n.toUInt8]
+  else if n < 0x800 then
+    [(0xC0 + n / 64).toUInt8, (0x80 + n % 64).toUInt8]
+  else if n < 0x10000 then
+    [(0xE0 + n / 4096).toUInt8, (0x80 + (n / 64) % 64).toUInt8, (0x80 + n % 64).toUInt8]
+  else
+    [(0xF0 + n / 262144).toUInt8, (0x80 + (n / 4096) % 64).toUInt8,
+     (0x80 + (n / 64) % 64).toUInt8, (0x80 + n % 64).toUInt8]
+
+/-- The bytes of a text. -/
+def encode (cs : List Char) : List UInt8 :=
+  cs.flatMap encodeChar
+
+/-- The payload bits of a continuation byte (80 to BF). -/
+def contVal (b : UInt8) : Option Nat :=
+  if 0x80 ≤ b.toNat ∧ b.toNat < 0xC0 then some (b.toNat - 0x80) else none
+
+/-- Strict decoding. The side conditions on the three and four
+    byte forms are the overlong, surrogate, and range rules:
+    after E0 the first continuation value is at least 32, after
+    ED it is below 32, after F0 it is at least 16, after F4 it
+    is below 16. -/
+def decode : List UInt8 → Option (List Char)
+  | [] => some []
+  | b :: rest =>
+    if b.toNat < 0x80 then
+      (decode rest).map fun cs => Char.ofNat b.toNat :: cs
+    else if b.toNat < 0xC2 then none
+    else if b.toNat < 0xE0 then
+      match rest with
+      | b1 :: rest1 =>
+        match contVal b1 with
+        | some v1 => (decode rest1).map fun cs =>
+            Char.ofNat ((b.toNat - 0xC0) * 64 + v1) :: cs
+        | none => none
+      | [] => none
+    else if b.toNat < 0xF0 then
+      match rest with
+      | b1 :: b2 :: rest1 =>
+        match contVal b1, contVal b2 with
+        | some v1, some v2 =>
+          if (b.toNat = 0xE0 → 0x20 ≤ v1) ∧ (b.toNat = 0xED → v1 < 0x20) then
+            (decode rest1).map fun cs =>
+              Char.ofNat ((b.toNat - 0xE0) * 4096 + v1 * 64 + v2) :: cs
+          else none
+        | _, _ => none
+      | _ => none
+    else if b.toNat < 0xF5 then
+      match rest with
+      | b1 :: b2 :: b3 :: rest1 =>
+        match contVal b1, contVal b2, contVal b3 with
+        | some v1, some v2, some v3 =>
+          if (b.toNat = 0xF0 → 0x10 ≤ v1) ∧ (b.toNat = 0xF4 → v1 < 0x10) then
+            (decode rest1).map fun cs =>
+              Char.ofNat ((b.toNat - 0xF0) * 262144 + v1 * 4096 + v2 * 64 + v3) :: cs
+          else none
+        | _, _, _ => none
+      | _ => none
+    else none
+
+end Mqtt.Utf8
diff --git a/Mqtt/Value.lean b/Mqtt/Value.lean
new file mode 100644
index 0000000..4261678
--- /dev/null
+++ b/Mqtt/Value.lean
@@ -0,0 +1,513 @@
+/-
+  MQTT 5.0 packet values and the printer.
+
+  A packet is one of the seven control packet types this slice
+  covers: CONNECT, PUBLISH, SUBSCRIBE, SUBACK, PINGREQ,
+  PINGRESP, and DISCONNECT. The printer writes a packet as the
+  fixed header byte, the remaining length as a variable byte
+  integer, and the body: the variable header and payload for the
+  packet's type.
+
+  Properties are held as an identifier and a typed value. The
+  value type of an identifier is fixed by the specification's
+  property table (section 2.2.2, Table 2-4), which also says
+  which packets a property may appear on. Will properties, the
+  property block inside a CONNECT packet's will, count as their
+  own packet kind for that table, as the specification's table
+  lists them on their own line.
+
+  Strings are held as lists of characters. What a string means
+  as bytes is settled by the strict UTF-8 codec in Mqtt/Utf8.
+-/
+
+import Mqtt.Utf8
+
+namespace Mqtt
+
+/-! ## Big endian byte strings -/
+
+/-- Write a number in exactly `k` bytes, most significant byte
+    first. Bytes past the number's own width are zero, and a
+    number too wide for `k` bytes loses its top bytes: the
+    printer only calls this with a width the number fits. -/
+def writeBE : Nat → Nat → List UInt8
+  | 0, _ => []
+  | k + 1, n => ((n / 256 ^ k) % 256).toUInt8 :: writeBE k (n % 256 ^ k)
+
+/-- The unfolding rule for `writeBE` at a successor width. -/
+theorem writeBE_succ (k n : Nat) :
+    writeBE (k + 1) n = ((n / 256 ^ k) % 256).toUInt8 :: writeBE k (n % 256 ^ k) := by
+  rw [writeBE]
+
+/-- A big endian writing is exactly as long as its width. -/
+theorem writeBE_length : ∀ (k n : Nat), (writeBE k n).length = k
+  | 0, _ => rfl
+  | k + 1, n => by rw [writeBE_succ]; simp [writeBE_length k]
+
+/-! ## The variable byte integer -/
+
+/-- Write a number as a variable byte integer (section 2.1.4):
+    seven bits per byte, low groups first, the top bit of each
+    byte but the last set as a continuation mark. The format
+    carries at most four bytes, so numbers below 2^28 are the
+    ones with a complete writing; a larger number loses its top
+    groups here, and the well formedness rules below keep every
+    written number under the bound. -/
+def printVBI (n : Nat) : List UInt8 :=
+  if n < 128 then [n.toUInt8]
+  else (128 + n % 128).toUInt8 :: printVBI (n / 128)
+termination_by n
+decreasing_by
+  exact Nat.div_lt_self (by omega) (by decide)
+
+/-- The unfolding rule for `printVBI`. -/
+theorem printVBI_def (n : Nat) :
+    printVBI n = if n < 128 then [n.toUInt8]
+      else (128 + n % 128).toUInt8 :: printVBI (n / 128) := by
+  rw [printVBI]
+
+/-! ## Properties: the table -/
+
+/-- The value type of a property, as the specification's
+    property table gives it. -/
+inductive PropType where
+  | byte : PropType
+  | twoByte : PropType
+  | fourByte : PropType
+  | varByte : PropType
+  | utf8 : PropType
+  | utf8Pair : PropType
+  | binary : PropType
+  deriving DecidableEq, Repr
+
+/-- A property value, in the shape of its type. Strings are
+    lists of characters; binary data is a list of bytes. -/
+inductive PropVal where
+  | byte (n : Nat) : PropVal
+  | twoByte (n : Nat) : PropVal
+  | fourByte (n : Nat) : PropVal
+  | varByte (n : Nat) : PropVal
+  | utf8 (s : List Char) : PropVal
+  | utf8Pair (k v : List Char) : PropVal
+  | binary (bs : List UInt8) : PropVal
+  deriving DecidableEq, Repr
+
+/-- The type of a property value. -/
+def valType : PropVal → PropType
+  | .byte _ => .byte
+  | .twoByte _ => .twoByte
+  | .fourByte _ => .fourByte
+  | .varByte _ => .varByte
+  | .utf8 _ => .utf8
+  | .utf8Pair _ _ => .utf8Pair
+  | .binary _ => .binary
+
+/-- One property: an identifier and a value. -/
+structure Property where
+  id : Nat
+  val : PropVal
+  deriving DecidableEq, Repr
+
+/-- The specification's property table (section 2.2.2,
+    Table 2-4): the value type of each identifier the
+    specification defines. An identifier the table does not
+    list has no type here, and the reader rejects it. -/
+def propTypeOf : Nat → Option PropType
+  | 0x01 => some .byte
+  | 0x02 => some .fourByte
+  | 0x03 => some .utf8
+  | 0x08 => some .utf8
+  | 0x09 => some .binary
+  | 0x0B => some .varByte
+  | 0x11 => some .fourByte
+  | 0x12 => some .utf8
+  | 0x13 => some .twoByte
+  | 0x15 => some .utf8
+  | 0x16 => some .binary
+  | 0x17 => some .byte
+  | 0x18 => some .fourByte
+  | 0x19 => some .byte
+  | 0x1A => some .utf8
+  | 0x1C => some .utf8
+  | 0x1F => some .utf8
+  | 0x21 => some .twoByte
+  | 0x22 => some .twoByte
+  | 0x23 => some .twoByte
+  | 0x24 => some .byte
+  | 0x25 => some .byte
+  | 0x26 => some .utf8Pair
+  | 0x27 => some .fourByte
+  | 0x28 => some .byte
+  | 0x29 => some .byte
+  | 0x2A => some .byte
+  | _ => none
+
+/-- The places a property block can stand, for the table's
+    packet column: the CONNECT packet's own block, the will
+    block inside CONNECT, and one block each for PUBLISH,
+    SUBSCRIBE, SUBACK, and DISCONNECT. -/
+inductive PropSet where
+  | connect : PropSet
+  | will : PropSet
+  | publish : PropSet
+  | subscribe : PropSet
+  | suback : PropSet
+  | disconnect : PropSet
+  deriving DecidableEq, Repr
+
+/-- The identifiers the specification's table allows on each
+    property block, by the table's packet column. -/
+def allowedOf : PropSet → List Nat
+  | .connect => [0x11, 0x15, 0x16, 0x17, 0x19, 0x21, 0x22, 0x26, 0x27]
+  | .will => [0x01, 0x02, 0x03, 0x08, 0x09, 0x18, 0x26]
+  | .publish => [0x01, 0x02, 0x03, 0x08, 0x09, 0x0B, 0x23, 0x26]
+  | .subscribe => [0x0B, 0x26]
+  | .suback => [0x1F, 0x26]
+  | .disconnect => [0x11, 0x1C, 0x1F, 0x26]
+
+/-- May this property appear more than once in one block? The
+    user property (0x26) may, wherever it is allowed. The
+    subscription identifier (0x0B) may repeat on PUBLISH: a
+    server sending one message for several matching
+    subscriptions carries one identifier per subscription, and
+    the identifiers may be equal (section 3.3.4). Every other
+    property is single use: a second copy in one block is
+    rejected. -/
+def repeatableIn (s : PropSet) (id : Nat) : Bool :=
+  id = 0x26 || (id = 0x0B && s = .publish)
+
+/-! ## String checks
+
+  The specification's string rules (section 1.5.4): a string is
+  well formed UTF-8 and must not contain the null character
+  U+0000. The byte length of a string field must also fit the
+  two byte length prefix. -/
+
+/-- Does this text contain the null character? -/
+def hasNul (s : List Char) : Bool :=
+  s.any fun c => decide (c = '\u0000')
+
+/-- A string fit to print: no null character, and its UTF-8
+    byte length fits the two byte length prefix. -/
+def StrWF (s : List Char) : Prop :=
+  '\u0000' ∉ s ∧ (Utf8.encode s).length ≤ 65535
+
+/-- Binary data fit to print: its length fits the two byte
+    length prefix. -/
+def BinWF (bs : List UInt8) : Prop :=
+  bs.length ≤ 65535
+
+/-- A topic name fit to print (section 4.7.1): a string, not
+    empty, holding neither wildcard character. -/
+def TopicWF (s : List Char) : Prop :=
+  StrWF s ∧ s ≠ [] ∧ '+' ∉ s ∧ '#' ∉ s
+
+/-! ## Field printers -/
+
+/-- Print a string field: the two byte length of its UTF-8
+    bytes, then the bytes (section 1.5.4). -/
+def printStr (s : List Char) : List UInt8 :=
+  writeBE 2 (Utf8.encode s).length ++ Utf8.encode s
+
+/-- Print a binary data field: the two byte length, then the
+    bytes (section 1.5.3). -/
+def printBin (bs : List UInt8) : List UInt8 :=
+  writeBE 2 bs.length ++ bs
+
+/-- Print a property value, in the shape of its type. -/
+def printPropVal : PropVal → List UInt8
+  | .byte n => [n.toUInt8]
+  | .twoByte n => writeBE 2 n
+  | .fourByte n => writeBE 4 n
+  | .varByte n => printVBI n
+  | .utf8 s => printStr s
+  | .utf8Pair k v => printStr k ++ printStr v
+  | .binary bs => printBin bs
+
+/-- Print one property: the identifier as a variable byte
+    integer, then the value. -/
+def printProperty (p : Property) : List UInt8 :=
+  printVBI p.id ++ printPropVal p.val
+
+/-- Print a list of properties, one after the other. -/
+def printPropsList : List Property → List UInt8
+  | [] => []
+  | p :: ps => printProperty p ++ printPropsList ps
+
+/-- Print a property block: the property length as a variable
+    byte integer, then the properties themselves (section
+    2.2.2). -/
+def printProps (ps : List Property) : List UInt8 :=
+  printVBI (printPropsList ps).length ++ printPropsList ps
+
+/-! ## The packet values -/
+
+/-- The subscription options of one topic filter in a SUBSCRIBE
+    packet (section 3.8.3): a maximum QoS, the no local and
+    retain as published flags, and a retain handling choice. -/
+structure SubOpts where
+  qos : Nat
+  noLocal : Bool
+  retainAsPublished : Bool
+  retainHandling : Nat
+  deriving DecidableEq, Repr
+
+/-- The options byte of a filter: QoS in bits 0 and 1, no local
+    at bit 2, retain as published at bit 3, retain handling in
+    bits 4 and 5, and the reserved bits 6 and 7 clear. -/
+def printOptsByte (o : SubOpts) : UInt8 :=
+  (o.qos + (if o.noLocal then 4 else 0) + (if o.retainAsPublished then 8 else 0)
+    + o.retainHandling * 16).toUInt8
+
+/-- A will, the part of a CONNECT packet that stands when its
+    will flag is set (section 3.1.3): will properties, a will
+    topic, and a will payload, with the QoS and retain flag the
+    connect flags byte carries. -/
+structure Will where
+  qos : Nat
+  retain : Bool
+  props : List Property
+  topic : List Char
+  payload : List UInt8
+  deriving DecidableEq, Repr
+
+/-- A CONNECT packet's fields (section 3.1). The protocol name
+    and level are not fields: this slice reads and writes MQTT
+    5.0 only, so they are fixed at "MQTT" and 5. The connect
+    flags byte is computed from the fields that drive it: the
+    username and password options, the will option with its QoS
+    and retain flag, and the clean start flag. -/
+structure Connect where
+  cleanStart : Bool
+  keepAlive : Nat
+  props : List Property
+  clientId : List Char
+  will : Option Will
+  username : Option (List Char)
+  password : Option (List UInt8)
+  deriving DecidableEq, Repr
+
+/-- A PUBLISH packet's fields (section 3.3). The packet
+    identifier stands exactly when the QoS is 1 or 2, so it is
+    an option beside the QoS. -/
+structure Publish where
+  dup : Bool
+  qos : Nat
+  retain : Bool
+  topic : List Char
+  packetId : Option Nat
+  props : List Property
+  payload : List UInt8
+  deriving DecidableEq, Repr
+
+/-- A control packet of one of the seven types this slice
+    covers. -/
+inductive Packet where
+  | connect (c : Connect) : Packet
+  | publish (p : Publish) : Packet
+  | subscribe (packetId : Nat) (props : List Property)
+      (filters : List (List Char × SubOpts)) : Packet
+  | suback (packetId : Nat) (props : List Property)
+      (reasons : List Nat) : Packet
+  | pingreq : Packet
+  | pingresp : Packet
+  | disconnect (body : Option (Nat × List Property)) : Packet
+  deriving DecidableEq, Repr
+
+/-! ## Body printers -/
+
+/-- The connect flags byte (section 3.1.2): username flag at
+    bit 7, password flag at bit 6, will retain at bit 5, will
+    QoS at bits 4 and 3, will flag at bit 2, clean start at
+    bit 1, and the reserved bit 0 clear. -/
+def connectFlags (c : Connect) : Nat :=
+  (if c.username.isSome then 128 else 0)
+    + (if c.password.isSome then 64 else 0)
+    + (match c.will with
+       | some w => (if w.retain then 32 else 0) + w.qos * 8 + 4
+       | none => 0)
+    + (if c.cleanStart then 2 else 0)
+
+/-- Print the will part of a CONNECT payload, or nothing when
+    there is no will. -/
+def printWillPart : Option Will → List UInt8
+  | none => []
+  | some w => printProps w.props ++ (printStr w.topic ++ printBin w.payload)
+
+/-- Print an optional string field, or nothing. -/
+def printOptStr : Option (List Char) → List UInt8
+  | none => []
+  | some s => printStr s
+
+/-- Print an optional binary field, or nothing. -/
+def printOptBin : Option (List UInt8) → List UInt8
+  | none => []
+  | some bs => printBin bs
+
+/-- The body of a CONNECT packet: the protocol name, protocol
+    level, connect flags, and keep alive, then the properties,
+    then the payload: client identifier, the will fields when
+    the will flag is set, the username when its flag is set,
+    and the password when its flag is set. -/
+def printConnectBody (c : Connect) : List UInt8 :=
+  printStr ['M', 'Q', 'T', 'T'] ++ ([5, (connectFlags c).toUInt8]
+    ++ (writeBE 2 c.keepAlive ++ (printProps c.props ++ (printStr c.clientId
+    ++ (printWillPart c.will ++ (printOptStr c.username
+    ++ printOptBin c.password))))))
+
+/-- The fixed header byte of a PUBLISH packet: the type 3, the
+    DUP flag at bit 3, the QoS at bits 2 and 1, and RETAIN at
+    bit 0. -/
+def publishHeader (p : Publish) : Nat :=
+  0x30 + (if p.dup then 8 else 0) + p.qos * 2 + (if p.retain then 1 else 0)
+
+/-- Print a packet identifier when one stands, or nothing. -/
+def printIdOpt : Option Nat → List UInt8
+  | none => []
+  | some id => writeBE 2 id
+
+/-- The body of a PUBLISH packet: topic name, the packet
+    identifier when the QoS carries one, the properties, then
+    the payload, which is all the bytes that remain. -/
+def printPublishBody (p : Publish) : List UInt8 :=
+  printStr p.topic ++ (printIdOpt p.packetId ++ (printProps p.props ++ p.payload))
+
+/-- Print one topic filter of a SUBSCRIBE payload: the filter
+    string, then its options byte. -/
+def printFilter (f : List Char × SubOpts) : List UInt8 :=
+  printStr f.1 ++ [printOptsByte f.2]
+
+/-- Print a list of topic filters, one after the other. -/
+def printFilters : List (List Char × SubOpts) → List UInt8
+  | [] => []
+  | f :: fs => printFilter f ++ printFilters fs
+
+/-- The body of a SUBSCRIBE packet: packet identifier,
+    properties, then the topic filters. -/
+def printSubscribeBody (id : Nat) (ps : List Property)
+    (fs : List (List Char × SubOpts)) : List UInt8 :=
+  writeBE 2 id ++ (printProps ps ++ printFilters fs)
+
+/-- The body of a SUBACK packet: packet identifier, properties,
+    then one reason code byte per granted subscription. -/
+def printSubackBody (id : Nat) (ps : List Property) (rs : List Nat) : List UInt8 :=
+  writeBE 2 id ++ (printProps ps ++ rs.map Nat.toUInt8)
+
+/-- The body of a packet: everything after the fixed header
+    byte and the remaining length. -/
+def bodyOf : Packet → List UInt8
+  | .connect c => printConnectBody c
+  | .publish p => printPublishBody p
+  | .subscribe id ps fs => printSubscribeBody id ps fs
+  | .suback id ps rs => printSubackBody id ps rs
+  | .pingreq => []
+  | .pingresp => []
+  | .disconnect none => []
+  | .disconnect (some (rc, ps)) => [rc.toUInt8] ++ printProps ps
+
+/-- The fixed header byte of a packet: the type in the high
+    nibble, and the flags the specification fixes in the low
+    nibble (section 2.1.2). SUBSCRIBE carries 0010; PUBLISH
+    carries its own DUP, QoS, and RETAIN bits; the rest carry
+    0000. -/
+def headerOf : Packet → UInt8
+  | .connect _ => 0x10
+  | .publish p => (publishHeader p).toUInt8
+  | .subscribe _ _ _ => 0x82
+  | .suback _ _ _ => 0x90
+  | .pingreq => 0xC0
+  | .pingresp => 0xD0
+  | .disconnect _ => 0xE0
+
+/-- Print a packet: the fixed header byte, the remaining length
+    as a variable byte integer, and the body. -/
+def print (p : Packet) : List UInt8 :=
+  headerOf p :: printVBI (bodyOf p).length ++ bodyOf p
+
+/-! ## Well formed values
+
+  The round trip claim in `Proofs` holds for well formed
+  packets: the fields the printer can write exactly. Numbers
+  fit the widths that carry them, strings obey the string
+  rules, properties match the table in type and place and do
+  not repeat a single use property, and the whole body fits
+  the remaining length's four byte variable byte integer. -/
+
+/-- A property value in the shape the printer writes exactly. -/
+def ValWF : PropVal → Prop
+  | .byte n => n < 256
+  | .twoByte n => n < 65536
+  | .fourByte n => n < 4294967296
+  | .varByte n => n < 268435456
+  | .utf8 s => StrWF s
+  | .utf8Pair k v => StrWF k ∧ StrWF v
+  | .binary bs => BinWF bs
+
+/-- A property list in the shape of one block: every property
+    is allowed on the block's packet kind, its value matches
+    the table's type for its identifier and is itself well
+    formed, and no single use property repeats. The `seen`
+    list carries the identifiers already standing in the
+    block; calls start it empty. -/
+def PropsWF (s : PropSet) : List Nat → List Property → Prop
+  | _, [] => True
+  | seen, p :: ps =>
+    p.id ∈ allowedOf s ∧ propTypeOf p.id = some (valType p.val) ∧ ValWF p.val
+      ∧ (repeatableIn s p.id = true ∨ p.id ∉ seen)
+      ∧ PropsWF s (p.id :: seen) ps
+
+/-- A property block fit to print: the list is well formed and
+    its printed length fits a variable byte integer. -/
+def PropsBlockWF (s : PropSet) (ps : List Property) : Prop :=
+  PropsWF s [] ps ∧ (printPropsList ps).length < 268435456
+
+/-- A will fit to print. -/
+def WillWF (w : Will) : Prop :=
+  w.qos ≤ 2 ∧ PropsBlockWF .will w.props ∧ TopicWF w.topic ∧ BinWF w.payload
+
+/-- A CONNECT packet fit to print. -/
+def ConnectWF (c : Connect) : Prop :=
+  c.keepAlive < 65536 ∧ PropsBlockWF .connect c.props ∧ StrWF c.clientId
+    ∧ (∀ w, c.will = some w → WillWF w)
+    ∧ (∀ u, c.username = some u → StrWF u)
+    ∧ (∀ p, c.password = some p → BinWF p)
+
+/-- A PUBLISH packet fit to print. The packet identifier
+    stands exactly when the QoS is 1 or 2, and is never 0. -/
+def PublishWF (p : Publish) : Prop :=
+  p.qos ≤ 2 ∧ TopicWF p.topic
+    ∧ (∀ id, p.packetId = some id → 1 ≤ id ∧ id < 65536 ∧ (p.qos = 1 ∨ p.qos = 2))
+    ∧ (p.packetId = none → p.qos = 0)
+    ∧ PropsBlockWF .publish p.props
+
+/-- Subscription options fit to print: the QoS and the retain
+    handling choice are at most 2 (3 is reserved in both). -/
+def OptsWF (o : SubOpts) : Prop :=
+  o.qos ≤ 2 ∧ o.retainHandling ≤ 2
+
+/-- A topic filter list fit to print, member by member. -/
+def FiltersWF : List (List Char × SubOpts) → Prop
+  | [] => True
+  | (f, o) :: fs => StrWF f ∧ OptsWF o ∧ FiltersWF fs
+
+/-- The per type half of well formedness for a packet. -/
+def PacketFieldsWF : Packet → Prop
+  | .connect c => ConnectWF c
+  | .publish p => PublishWF p
+  | .subscribe id ps fs =>
+    1 ≤ id ∧ id < 65536 ∧ PropsBlockWF .subscribe ps ∧ fs ≠ [] ∧ FiltersWF fs
+  | .suback id ps rs =>
+    1 ≤ id ∧ id < 65536 ∧ PropsBlockWF .suback ps ∧ rs ≠ []
+      ∧ (∀ r ∈ rs, r < 256)
+  | .pingreq => True
+  | .pingresp => True
+  | .disconnect none => True
+  | .disconnect (some (rc, ps)) => rc < 256 ∧ PropsBlockWF .disconnect ps
+
+/-- A packet fit to print: its fields are well formed and its
+    body fits the remaining length, a variable byte integer of
+    at most four bytes. -/
+def PacketWF (p : Packet) : Prop :=
+  PacketFieldsWF p ∧ (bodyOf p).length < 268435456
+
+end Mqtt
diff --git a/Mqtt/Verify.lean b/Mqtt/Verify.lean
new file mode 100644
index 0000000..1d0b3a7
--- /dev/null
+++ b/Mqtt/Verify.lean
@@ -0,0 +1,22 @@
+/-
+  Axiom check for the claims this package makes. Run with:
+
+    lake env lean Mqtt/Verify.lean
+
+  Every claim should list only the standard axioms (propext,
+  Classical.choice, Quot.sound). A line naming sorryAx would mean
+  a proof rests on an admitted gap, and the claim is not proved.
+-/
+
+import Proofs
+import Proofs.Examples
+
+open Mqtt.Proofs Mqtt.Examples
+
+#print axioms parse_print
+#print axioms parsePacket_print
+#print axioms decVBI_printVBI
+#print axioms parse_connect
+#print axioms parse_publish_qos1
+#print axioms vbi_max
+#print axioms vbi_five_bytes
diff --git a/Proofs.lean b/Proofs.lean
new file mode 100644
index 0000000..6bfe916
--- /dev/null
+++ b/Proofs.lean
@@ -0,0 +1,4 @@
+import Proofs.Utf8
+import Proofs.RoundTrip
+import Proofs.Examples
+import Proofs.SpecProofs
diff --git a/Proofs/Examples.lean b/Proofs/Examples.lean
new file mode 100644
index 0000000..6a49abf
--- /dev/null
+++ b/Proofs/Examples.lean
@@ -0,0 +1,105 @@
+/-
+  Worked examples, proved. The variable byte integer examples
+  are the MQTT 5.0 specification's own table (section 2.1.4).
+  The packet examples are hand built from the specification
+  text, one for each packet type in this slice, plus the
+  rejections this slice promises. The same packets run
+  through the command line tool in the test harness, where
+  they are checked byte by byte a second time.
+
+  The examples are stated on the reading side. The printer's
+  variable byte integer is defined by well founded recursion,
+  which the kernel will not evaluate here; the round trip
+  theorem covers the printer instead.
+-/
+
+import Mqtt
+
+namespace Mqtt.Examples
+
+open Mqtt
+
+/-! ## The variable byte integer table (spec section 2.1.4) -/
+
+theorem vbi_zero : decVBI [0] = some (0, []) := by decide
+
+theorem vbi_127 : decVBI [127] = some (127, []) := by decide
+
+theorem vbi_128 : decVBI [128, 1] = some (128, []) := by decide
+
+theorem vbi_16383 : decVBI [255, 127] = some (16383, []) := by decide
+
+theorem vbi_16384 : decVBI [128, 128, 1] = some (16384, []) := by decide
+
+theorem vbi_2097151 : decVBI [255, 255, 127] = some (2097151, []) := by
+  decide
+
+theorem vbi_2097152 : decVBI [128, 128, 128, 1] = some (2097152, []) := by
+  decide
+
+theorem vbi_max : decVBI [255, 255, 255, 127] = some (268435455, []) := by
+  decide
+
+/-- A continuation bit on the fourth byte rejects: the value
+    would need a fifth byte. -/
+theorem vbi_five_bytes : decVBI [255, 255, 255, 255] = none := by decide
+
+/-- The pinned reading: a non minimal encoding within four
+    bytes is accepted. Here 0 carried in two bytes. -/
+theorem vbi_non_minimal : decVBI [128, 0] = some (0, []) := by decide
+
+/-- The decoder returns the rest of the stream untouched. -/
+theorem vbi_rest : decVBI [128, 1, 99] = some (128, [99]) := by decide
+
+/-! ## One packet of each type -/
+
+theorem parse_pingreq : parse [192, 0] = some .pingreq := by decide
+
+theorem parse_pingresp : parse [208, 0] = some .pingresp := by decide
+
+/-- A DISCONNECT with no body is a normal disconnection. -/
+theorem parse_disconnect_empty :
+    parse [224, 0] = some (.disconnect none) := by decide
+
+/-- A DISCONNECT body of one byte is a reason code with an
+    empty property block. It is legal. -/
+theorem parse_disconnect_reason :
+    parse [224, 1, 0] = some (.disconnect (some (0, []))) := by decide
+
+theorem parse_publish_qos0 :
+    parse [48, 6, 0, 1, 97, 0, 1, 2]
+      = some (.publish ⟨false, 0, false, ['a'], none, [], [1, 2]⟩) := by
+  decide
+
+theorem parse_publish_qos1 :
+    parse [50, 6, 0, 1, 97, 0, 1, 0]
+      = some (.publish ⟨false, 1, false, ['a'], some 1, [], []⟩) := by
+  decide
+
+theorem parse_subscribe :
+    parse [130, 7, 0, 1, 0, 0, 1, 97, 0]
+      = some (.subscribe 1 [] [(['a'], ⟨0, false, false, 0⟩)]) := by
+  decide
+
+theorem parse_suback :
+    parse [144, 4, 0, 1, 0, 0] = some (.suback 1 [] [0]) := by decide
+
+theorem parse_connect :
+    parse [16, 14, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 0, 0, 1, 120]
+      = some (.connect ⟨true, 0, [], ['x'], none, none, none⟩) := by
+  decide
+
+/-! ## Rejections -/
+
+/-- A PINGREQ with a body rejects: its remaining length must
+    be 0. -/
+theorem parse_pingreq_body : parse [192, 1, 0] = none := by decide
+
+/-- An empty PUBLISH topic rejects. -/
+theorem parse_publish_empty_topic : parse [48, 2, 0, 0] = none := by
+  decide
+
+/-- A packet type outside this slice rejects, here type 2. -/
+theorem parse_wrong_type : parse [32, 0] = none := by decide
+
+end Mqtt.Examples
diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean
new file mode 100644
index 0000000..c3fcadc
--- /dev/null
+++ b/Proofs/RoundTrip.lean
@@ -0,0 +1,1221 @@
+/-
+  The round trip proofs for the MQTT packet codec: reading what
+  the printer wrote gives the packet back.
+
+  The main claim is `Mqtt.Proofs.parse_print`: for a well
+  formed packet `p`, `parse (print p) = some p`. It is built
+  from one lemma per field reader, each in the shape "reading
+  the printed field, with any bytes after it left in place,
+  gives the field and leaves the bytes after it". Property
+  blocks and filter lists read to the end of their bytes, so
+  their lemmas are stated on the printed bytes exactly.
+-/
+
+import Mqtt
+import Proofs.Utf8
+
+namespace Mqtt.Proofs
+
+open Mqtt
+
+/-- A number below 256 written as a byte reads back as itself. -/
+theorem toNat_toUInt8 {k : Nat} (h : k < 256) : k.toUInt8.toNat = k :=
+  Mqtt.Utf8.Proofs.toNat_toUInt8 h
+
+/-! ## The byte readers on writings -/
+
+/-- A big endian writing reads back: at every width, the number
+    written is the number read, and the bytes after the writing
+    are left alone. -/
+theorem readNat_writeBE : ∀ (k n : Nat) (rest : List UInt8),
+    n < 256 ^ k → readNat k (writeBE k n ++ rest) = some (n, rest) := by
+  intro k
+  induction k with
+  | zero =>
+    intro n rest hn
+    rw [Nat.pow_zero] at hn
+    have hn0 : n = 0 := by omega
+    rw [hn0]
+    rfl
+  | succ k ih =>
+    intro n rest hn
+    have hP : 0 < 256 ^ k := Nat.pow_pos (by decide)
+    have hlt : n / 256 ^ k < 256 := by
+      rw [Nat.pow_succ] at hn
+      exact Nat.div_lt_of_lt_mul hn
+    have hd : ((n / 256 ^ k) % 256).toUInt8.toNat = n / 256 ^ k := by
+      have h1 : ((n / 256 ^ k) % 256).toUInt8.toNat = (n / 256 ^ k) % 256 :=
+        UInt8.toNat_ofNat_of_lt (Nat.mod_lt _ (by decide : 0 < 256))
+      rw [h1, Nat.mod_eq_of_lt hlt]
+    rw [writeBE_succ, List.cons_append, readNat_succ_cons,
+      ih (n % 256 ^ k) rest (Nat.mod_lt _ hP), hd]
+    simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq]
+    constructor
+    · rw [Nat.mul_comm]; exact Nat.div_add_mod _ _
+    · trivial
+
+/-- A byte run reads back whole: taking the front of a list that
+    starts with the run gives the run, and leaves the rest. -/
+theorem readBytes_append : ∀ (n : Nat) (bs rest : List UInt8),
+    bs.length = n → readBytes n (bs ++ rest) = some (bs, rest) := by
+  intro n bs rest h
+  unfold readBytes
+  rw [if_pos (by simp [List.length_append, h] : (bs ++ rest).length ≥ n),
+    ← h, List.take_left, List.drop_left]
+
+/-! ## The variable byte integer -/
+
+/-- A variable byte integer writing is never empty. -/
+theorem printVBI_pos : ∀ (n : Nat), 0 < (printVBI n).length := by
+  intro n
+  rw [printVBI_def]
+  by_cases h : n < 128
+  · rw [if_pos h]; simp
+  · rw [if_neg h]; simp
+
+/-- Reading a printed variable byte integer, with the counting
+    form of the reader: with at most `k + 1` bytes to spend and
+    a value that fits in `k + 1` groups, the reader returns the
+    accumulated value and leaves the bytes after the writing.
+    Induction on `k`: a value below 128 is one byte, and a
+    larger value is its low group, marked as continued, in
+    front of the writing of the rest of the value. -/
+theorem decVBIGo_printVBI : ∀ (k : Nat) (n acc mult : Nat) (rest : List UInt8),
+    n < 128 ^ (k + 1) →
+    decVBIGo (k + 1) acc mult (printVBI n ++ rest) = some (acc + mult * n, rest) := by
+  intro k
+  induction k with
+  | zero =>
+    intro n acc mult rest hn
+    rw [Nat.pow_one] at hn
+    rw [printVBI_def, if_pos hn]
+    show decVBIGo 1 acc mult (n.toUInt8 :: rest) = some (acc + mult * n, rest)
+    rw [decVBIGo, if_pos (by rw [toNat_toUInt8 (by omega : n < 256)]; exact hn),
+      toNat_toUInt8 (by omega : n < 256)]
+  | succ k ih =>
+    intro n acc mult rest hn
+    by_cases h1 : n < 128
+    · rw [printVBI_def, if_pos h1]
+      show decVBIGo (k + 2) acc mult (n.toUInt8 :: rest) = some (acc + mult * n, rest)
+      rw [decVBIGo, if_pos (by rw [toNat_toUInt8 (by omega : n < 256)]; exact h1),
+        toNat_toUInt8 (by omega : n < 256)]
+    · have hmod : n % 128 < 128 := Nat.mod_lt _ (by decide)
+      rw [printVBI_def, if_neg h1]
+      show decVBIGo (k + 2) acc mult
+          ((128 + n % 128).toUInt8 :: (printVBI (n / 128) ++ rest)) =
+        some (acc + mult * n, rest)
+      rw [decVBIGo, toNat_toUInt8 (by omega : 128 + n % 128 < 256),
+        if_neg (by omega : ¬ (128 + n % 128 < 128)),
+        if_neg (by omega : ¬ k + 2 ≤ 1), Nat.add_sub_cancel_left]
+      show decVBIGo (k + 1) (acc + mult * (n % 128)) (mult * 128)
+          (printVBI (n / 128) ++ rest) = some (acc + mult * n, rest)
+      have hdiv : n / 128 < 128 ^ (k + 1) := by
+        rw [Nat.pow_succ] at hn
+        omega
+      rw [ih (n / 128) (acc + mult * (n % 128)) (mult * 128) rest hdiv]
+      have key : acc + mult * (n % 128) + mult * 128 * (n / 128) = acc + mult * n := by
+        have h := Nat.mod_add_div n 128
+        have h3 : mult * (n % 128) + mult * 128 * (n / 128) = mult * n := by
+          rw [Nat.mul_assoc, ← Nat.left_distrib, h]
+        omega
+      rw [key]
+
+/-- Reading a printed variable byte integer gives the number
+    back: any number below 2^28, the most four bytes carry. -/
+theorem decVBI_printVBI (n : Nat) (rest : List UInt8) (hn : n < 268435456) :
+    decVBI (printVBI n ++ rest) = some (n, rest) := by
+  have e : (128 : Nat) ^ (3 + 1) = 268435456 := by decide
+  rw [← e] at hn
+  have h := decVBIGo_printVBI 3 n 0 1 rest hn
+  simpa [decVBI] using h
+
+/-! ## Step lemmas
+
+  The readers written with `do` notation are unfolded one step
+  at a time through these equations, each proved by `rfl`, so
+  the proofs below can rewrite one field at a time. -/
+
+/-- One step of the string reader, stated for rewriting. -/
+theorem readStr_step (bs : List UInt8) :
+    readStr bs = (readNat 2 bs).bind fun (len, r1) =>
+      (readBytes len r1).bind fun (chunk, r2) =>
+      ((Utf8.decode chunk).bind checkChars).bind fun s => some (s, r2) := rfl
+
+/-- One step of the binary reader, stated for rewriting. -/
+theorem readBin_step (bs : List UInt8) :
+    readBin bs = (readNat 2 bs).bind fun (len, r1) => readBytes len r1 := rfl
+
+/-- One step of the string pair value reader, stated for
+    rewriting. -/
+theorem readPropVal_pair_step (bs : List UInt8) :
+    readPropVal .utf8Pair bs = (readStr bs).bind fun (k, r1) =>
+      (readStr r1).bind fun (v, r2) => some (.utf8Pair k v, r2) := rfl
+
+/-- One step of the property reader, stated for rewriting. -/
+theorem readEntry_step (s : PropSet) (seen : List Nat) (bs : List UInt8) :
+    readEntry s seen bs = (decVBI bs).bind fun (id, r1) =>
+      if (allowedOf s).contains id && (repeatableIn s id || !seen.contains id) then
+        match propTypeOf id with
+        | none => none
+        | some t => (readPropVal t r1).map fun (v, r2) => (⟨id, v⟩, r2)
+      else none := rfl
+
+/-- One step of the property block reader, stated for
+    rewriting. -/
+theorem readProps_step (s : PropSet) (bs : List UInt8) :
+    readProps s bs = (decVBI bs).bind fun (len, r1) =>
+      (readBytes len r1).bind fun (seg, r2) =>
+      (readEntries s seg).bind fun ps => some (ps, r2) := rfl
+
+/-! ## Strings and binary data -/
+
+/-- The null character check passes on a well formed string. -/
+theorem hasNul_false {s : List Char} (h : '\u0000' ∉ s) : hasNul s = false := by
+  simp only [hasNul, List.any_eq_false]
+  intro c hc hcc
+  have hceq : c = '\u0000' := of_decide_eq_true hcc
+  subst hceq
+  exact h hc
+
+/-- The character check passes on a well formed string. -/
+theorem checkChars_of_wf {s : List Char} (h : StrWF s) : checkChars s = some s := by
+  simp [checkChars, hasNul_false h.1]
+
+/-- A printed string field reads back: the string, with the
+    bytes after the field left in place. -/
+theorem readStr_printStr (s : List Char) (rest : List UInt8) (h : StrWF s) :
+    readStr (printStr s ++ rest) = some (s, rest) := by
+  have hlen : (Utf8.encode s).length < 256 ^ 2 := by
+    have h2 := h.2
+    have e : (256 : Nat) ^ 2 = 65536 := by decide
+    rw [e]
+    omega
+  rw [readStr_step, printStr, List.append_assoc, readNat_writeBE 2 _ _ hlen]
+  simp only [Option.bind_some]
+  rw [readBytes_append _ _ _ rfl]
+  simp only [Option.bind_some]
+  rw [Mqtt.Utf8.Proofs.decode_encode]
+  simp only [Option.bind_some]
+  rw [checkChars_of_wf h]
+  simp only [Option.bind_some]
+
+/-- A printed binary field reads back: the bytes, with the
+    bytes after the field left in place. -/
+theorem readBin_printBin (bs : List UInt8) (rest : List UInt8) (h : BinWF bs) :
+    readBin (printBin bs ++ rest) = some (bs, rest) := by
+  have hlen : bs.length < 256 ^ 2 := by
+    have h2 : bs.length ≤ 65535 := h
+    have e : (256 : Nat) ^ 2 = 65536 := by decide
+    rw [e]
+    omega
+  rw [readBin_step, printBin, List.append_assoc, readNat_writeBE 2 _ _ hlen]
+  simp only [Option.bind_some]
+  rw [readBytes_append _ _ _ rfl]
+
+/-! ## Properties -/
+
+/-- An identifier with a table entry is below 2^28. -/
+theorem propTypeOf_id_lt {id : Nat} {t : PropType}
+    (h : propTypeOf id = some t) : id < 268435456 := by
+  unfold propTypeOf at h
+  split at h <;> simp_all <;> omega
+
+/-- A printed property value reads back, at the type the table
+    gives it. -/
+theorem readPropVal_printPropVal (v : PropVal) (rest : List UInt8) (h : ValWF v) :
+    readPropVal (valType v) (printPropVal v ++ rest) = some (v, rest) := by
+  cases v with
+  | byte n =>
+    have hn : n < 256 := h
+    simp only [valType, printPropVal, readPropVal]
+    rw [List.cons_append, List.nil_append, readNat_succ_cons,
+      show readNat 0 rest = some (0, rest) from rfl, Option.map_some,
+      Option.map_some, toNat_toUInt8 hn]
+    simp
+  | twoByte n =>
+    simp only [valType, printPropVal, readPropVal]
+    rw [readNat_writeBE 2 n rest (by
+      have e : (256 : Nat) ^ 2 = 65536 := by decide
+      rw [e]; exact h)]
+    rfl
+  | fourByte n =>
+    simp only [valType, printPropVal, readPropVal]
+    rw [readNat_writeBE 4 n rest (by
+      have e : (256 : Nat) ^ 4 = 4294967296 := by decide
+      rw [e]; exact h)]
+    rfl
+  | varByte n =>
+    simp only [valType, printPropVal, readPropVal]
+    rw [decVBI_printVBI n rest h]
+    rfl
+  | utf8 s =>
+    simp only [valType, printPropVal, readPropVal]
+    rw [readStr_printStr s rest h]
+    rfl
+  | utf8Pair k v =>
+    obtain ⟨hk, hv⟩ := h
+    show readPropVal .utf8Pair ((printStr k ++ printStr v) ++ rest)
+        = some (.utf8Pair k v, rest)
+    rw [readPropVal_pair_step, List.append_assoc, readStr_printStr k _ hk]
+    simp only [Option.bind_some]
+    rw [readStr_printStr v rest hv]
+    simp only [Option.bind_some]
+  | binary bs =>
+    simp only [valType, printPropVal, readPropVal]
+    rw [readBin_printBin bs rest h]
+    rfl
+
+/-- A printed property reads back, when the property stands in
+    the block it is read for: its identifier is allowed there,
+    its value matches the table's type, the value is well
+    formed, and the block's repeat rule is respected. -/
+theorem readEntry_printProperty (s : PropSet) (seen : List Nat) (p : Property)
+    (rest : List UInt8)
+    (hid : p.id ∈ allowedOf s) (hty : propTypeOf p.id = some (valType p.val))
+    (hval : ValWF p.val)
+    (hrep : repeatableIn s p.id = true ∨ p.id ∉ seen) :
+    readEntry s seen (printProperty p ++ rest) = some (p, rest) := by
+  have hc : (allowedOf s).contains p.id = true := List.contains_iff_mem.mpr hid
+  have hr : (repeatableIn s p.id || !seen.contains p.id) = true := by
+    cases hrep with
+    | inl h => rw [h]; rfl
+    | inr h =>
+      have h2 : seen.contains p.id = false := by
+        cases hseen : seen.contains p.id with
+        | false => rfl
+        | true => exact absurd (List.contains_iff_mem.mp hseen) h
+      rw [h2]
+      cases repeatableIn s p.id <;> rfl
+  rw [readEntry_step, printProperty, List.append_assoc,
+    decVBI_printVBI p.id _ (propTypeOf_id_lt hty)]
+  simp only [Option.bind_some]
+  rw [if_pos (by rw [hc, hr]; rfl), hty]
+  simp only []
+  rw [readPropVal_printPropVal p.val rest hval]
+  rfl
+
+/-- A printed property list reads back whole, when the list is
+    well formed for its block: the reader spends one fuel per
+    property and each property takes at least a byte, so the
+    list's own length is fuel enough. -/
+theorem readEntriesGo_printPropsList : ∀ (fuel : Nat) (s : PropSet)
+    (seen : List Nat) (ps : List Property),
+    ps.length ≤ fuel → PropsWF s seen ps →
+    readEntriesGo fuel s seen (printPropsList ps) = some (ps, []) := by
+  intro fuel
+  induction fuel with
+  | zero =>
+    intro s seen ps hlen _
+    have hps : ps = [] := by
+      cases ps with
+      | nil => rfl
+      | cons p ps' => simp at hlen
+    rw [hps]
+    rfl
+  | succ fuel ih =>
+    intro s seen ps hlen hwf
+    cases ps with
+    | nil => rfl
+    | cons p ps' =>
+      have hne : ¬ (printProperty p ++ printPropsList ps').isEmpty := by
+        have h1 : 0 < (printVBI p.id).length := printVBI_pos p.id
+        intro hcon
+        rw [List.isEmpty_iff] at hcon
+        have h3 : printProperty p = [] := (List.append_eq_nil_iff.mp hcon).1
+        rw [printProperty] at h3
+        have h4 : printVBI p.id = [] := (List.append_eq_nil_iff.mp h3).1
+        rw [h4] at h1
+        exact absurd h1 (by decide)
+      obtain ⟨hid, hty, hval, hrep, htail⟩ := hwf
+      rw [List.length_cons] at hlen
+      show readEntriesGo (fuel + 1) s seen (printPropsList (p :: ps')) = _
+      rw [printPropsList, readEntriesGo, if_neg hne,
+        readEntry_printProperty s seen p (printPropsList ps') hid hty hval hrep]
+      simp only []
+      rw [ih s (p.id :: seen) ps' (by omega) htail]
+
+/-- A property list is never longer than its printing: each
+    property takes at least the byte of its identifier. -/
+theorem propsList_length_le (ps : List Property) :
+    ps.length ≤ (printPropsList ps).length := by
+  induction ps with
+  | nil => simp [printPropsList]
+  | cons p ps' ih =>
+    have h1 : 0 < (printVBI p.id).length := printVBI_pos p.id
+    simp only [printPropsList, printProperty, List.length_cons,
+      List.length_append]
+    omega
+
+/-- A whole printed property block's insides read back. -/
+theorem readEntries_printPropsList (s : PropSet) (ps : List Property)
+    (h : PropsWF s [] ps) : readEntries s (printPropsList ps) = some ps := by
+  unfold readEntries
+  rw [readEntriesGo_printPropsList (printPropsList ps).length s [] ps
+    (propsList_length_le ps) h]
+
+/-- A printed property block reads back: the properties, with
+    the bytes after the block left in place. -/
+theorem readProps_printProps (s : PropSet) (ps : List Property)
+    (rest : List UInt8) (h : PropsBlockWF s ps) :
+    readProps s (printProps ps ++ rest) = some (ps, rest) := by
+  obtain ⟨hwf, hlen⟩ := h
+  rw [readProps_step, printProps, List.append_assoc, decVBI_printVBI _ _ hlen]
+  simp only [Option.bind_some]
+  rw [readBytes_append _ _ _ rfl]
+  simp only [Option.bind_some]
+  rw [readEntries_printPropsList s ps hwf]
+  simp only [Option.bind_some]
+
+/-! ## Topic names and flag bits -/
+
+/-- An `any` test for one character fails when the character
+    does not stand in the text. -/
+theorem any_eq_false_of_not_mem {s : List Char} {c : Char} (h : c ∉ s) :
+    s.any (fun x => decide (x = c)) = false := by
+  simp only [List.any_eq_false]
+  intro x hx hxc
+  have hxcq : x = c := of_decide_eq_true hxc
+  subst hxcq
+  exact h hx
+
+/-- The topic name check passes on a well formed topic name. -/
+theorem checkTopic_of_wf {s : List Char} (h : TopicWF s) : checkTopic s = some s := by
+  obtain ⟨hstr, hne, hp, hh⟩ := h
+  have e1 : s.isEmpty = false := by
+    cases s with
+    | nil => exact absurd rfl hne
+    | cons a t => rfl
+  have e2 : s.any (fun c => decide (c = '+')) = false :=
+    any_eq_false_of_not_mem hp
+  have e3 : s.any (fun c => decide (c = '#')) = false :=
+    any_eq_false_of_not_mem hh
+  unfold checkTopic
+  rw [e1, e2, e3]
+  exact if_neg (by decide)
+
+/-- An `if` on a boolean, in the flags builders' shape, is the
+    bit as a number times the place value. -/
+theorem if_bool_mul (b : Bool) (x : Nat) :
+    (if b then x else 0) = (if b then 1 else 0) * x := by
+  cases b <;> simp
+
+/-- The bits of a number built as `q + a * 4 + b * 8 + rh * 16`,
+    with `a` and `b` bits and `q` and `rh` at most 2: the fields
+    an options byte carries. Pure arithmetic. -/
+theorem optsByte_fields (q rh a b : Nat) (hq : q ≤ 2) (hr : rh ≤ 2)
+    (ha : a ≤ 1) (hb : b ≤ 1) :
+    readOptsByte (q + a * 4 + b * 8 + rh * 16) = some ⟨q, a = 1, b = 1, rh⟩ := by
+  unfold readOptsByte
+  rw [if_pos ⟨by omega, by omega, by omega⟩]
+  simp only [Option.some.injEq, SubOpts.mk.injEq]
+  refine ⟨by omega, ?_, ?_, by omega⟩
+  · rw [show (q + a * 4 + b * 8 + rh * 16) / 4 % 2 = a by omega]
+  · rw [show (q + a * 4 + b * 8 + rh * 16) / 8 % 2 = b by omega]
+
+/-- A printed options byte reads back as the options. -/
+theorem readOptsByte_printOptsByte (o : SubOpts) (h : OptsWF o) :
+    readOptsByte (printOptsByte o).toNat = some o := by
+  obtain ⟨q, nl, rap, rh⟩ := o
+  have hq : q ≤ 2 := h.1
+  have hr : rh ≤ 2 := h.2
+  have ha : (if nl then (1 : Nat) else 0) ≤ 1 := by cases nl <;> decide
+  have hb : (if rap then (1 : Nat) else 0) ≤ 1 := by cases rap <;> decide
+  have hbound : q + (if nl then 1 else 0) * 4 + (if rap then 1 else 0) * 8
+      + rh * 16 < 256 := by omega
+  have hsum : (printOptsByte ⟨q, nl, rap, rh⟩).toNat
+      = q + (if nl then 1 else 0) * 4 + (if rap then 1 else 0) * 8 + rh * 16 := by
+    show ((q + (if nl then 4 else 0) + (if rap then 8 else 0) + rh * 16).toUInt8).toNat = _
+    rw [if_bool_mul nl 4, if_bool_mul rap 8, toNat_toUInt8 hbound]
+  rw [hsum, optsByte_fields q rh _ _ hq hr ha hb]
+  cases nl <;> cases rap <;> rfl
+
+/-! ## SUBSCRIBE filters -/
+
+/-- A printed filter list is at least as long as the list: each
+    filter takes at least the byte of its options. -/
+theorem printFilters_length_ge : ∀ (fs : List (List Char × SubOpts)),
+    fs.length ≤ (printFilters fs).length := by
+  intro fs
+  induction fs with
+  | nil => simp [printFilters]
+  | cons f fs' ih =>
+    have h1 : 0 < (printFilter f).length := by
+      simp only [printFilter, List.length_append, List.length_cons,
+        List.length_nil]
+      omega
+    simp only [printFilters, List.length_cons, List.length_append]
+    omega
+
+/-- A printed filter list reads back whole, when its members
+    are well formed: the reader spends one fuel per filter and
+    each filter takes at least a byte, so the list's own length
+    is fuel enough. -/
+theorem readFiltersGo_printFilters : ∀ (fuel : Nat)
+    (fs : List (List Char × SubOpts)),
+    fs.length ≤ fuel → FiltersWF fs →
+    readFiltersGo fuel (printFilters fs) = some (fs, []) := by
+  intro fuel
+  induction fuel with
+  | zero =>
+    intro fs hlen _
+    have hfs : fs = [] := by
+      cases fs with
+      | nil => rfl
+      | cons f fs' => simp at hlen
+    rw [hfs]
+    rfl
+  | succ fuel ih =>
+    intro fs hlen hwf
+    cases fs with
+    | nil => rfl
+    | cons fr fs' =>
+      obtain ⟨f, o⟩ := fr
+      obtain ⟨hf, ho, htail⟩ := hwf
+      have hne : ¬ (printFilter (f, o) ++ printFilters fs').isEmpty := by
+        have h1 : 0 < (printFilter (f, o)).length := by
+          simp only [printFilter, List.length_append, List.length_cons,
+            List.length_nil]
+          omega
+        intro hcon
+        rw [List.isEmpty_iff] at hcon
+        have h3 : printFilter (f, o) = [] := (List.append_eq_nil_iff.mp hcon).1
+        rw [h3] at h1
+        exact absurd h1 (by decide)
+      rw [List.length_cons] at hlen
+      show readFiltersGo (fuel + 1) (printFilters ((f, o) :: fs')) = _
+      rw [printFilters, readFiltersGo, if_neg hne, printFilter,
+        List.append_assoc, readStr_printStr f _ hf]
+      rw [List.cons_append, List.nil_append]
+      simp only []
+      rw [readOptsByte_printOptsByte o ho]
+      simp only []
+      rw [ih fs' (by omega) htail]
+
+/-! ## Packet bodies -/
+
+/-- One step of the single byte reader, stated for rewriting. -/
+theorem readByte_cons (b : UInt8) (bs : List UInt8) :
+    readByte (b :: bs) = some (b.toNat, bs) := rfl
+
+/-- The bits of a PUBLISH flags nibble built from a packet's
+    fields: the QoS sits at bits 2 and 1, DUP at bit 3, RETAIN
+    at bit 0. -/
+theorem publish_bits (dup retain : Bool) (qos : Nat) (hq : qos ≤ 2) :
+    ((if dup then 8 else 0) + qos * 2 + (if retain then 1 else 0)) / 2 % 4 = qos
+      ∧ flagBit ((if dup then 8 else 0) + qos * 2 + (if retain then 1 else 0)) 3 = dup
+      ∧ flagBit ((if dup then 8 else 0) + qos * 2 + (if retain then 1 else 0)) 0
+        = retain := by
+  have e1 : (if dup then (8 : Nat) else 0) = (if dup then 1 else 0) * 8 :=
+    if_bool_mul dup 8
+  have e2 : (if retain then (1 : Nat) else 0) = (if retain then 1 else 0) * 1 :=
+    if_bool_mul retain 1
+  have ha : (if dup then (1 : Nat) else 0) ≤ 1 := by cases dup <;> decide
+  have hb : (if retain then (1 : Nat) else 0) ≤ 1 := by cases retain <;> decide
+  rw [e1, e2]
+  refine ⟨by omega, ?_, ?_⟩
+  · unfold flagBit
+    rw [show (2 : Nat) ^ 3 = 8 by decide,
+      show ((if dup then 1 else 0) * 8 + qos * 2 + (if retain then 1 else 0) * 1)
+          / 8 % 2 = (if dup then 1 else 0) by omega]
+    cases dup <;> rfl
+  · unfold flagBit
+    rw [show (2 : Nat) ^ 0 = 1 by decide,
+      show ((if dup then 1 else 0) * 8 + qos * 2 + (if retain then 1 else 0) * 1)
+          / 1 % 2 = (if retain then 1 else 0) by omega]
+    cases retain <;> rfl
+
+/-- The properties reader on exactly the printed bytes. -/
+theorem readProps_printProps_exact (s : PropSet) (ps : List Property)
+    (h : PropsBlockWF s ps) : readProps s (printProps ps) = some (ps, []) := by
+  have h2 := readProps_printProps s ps [] h
+  rwa [List.append_nil] at h2
+
+/-- The SUBSCRIBE body reader as one bind chain; the form the
+    round trip proof rewrites through. -/
+theorem readSubscribeBody_step (seg : List UInt8) :
+    readSubscribeBody seg =
+    (readNat 2 seg).bind fun (id, r1) =>
+      if id ≠ 0 then
+        (readProps .subscribe r1).bind fun (props, r2) =>
+        (readFiltersGo r2.length r2).bind fun (fs, r3) =>
+          if r3.isEmpty && !fs.isEmpty then some (.subscribe id props fs)
+          else none
+      else none := rfl
+
+/-- A printed SUBSCRIBE body reads back as the packet. -/
+theorem readSubscribeBody_printSubscribeBody (id : Nat) (ps : List Property)
+    (fs : List (List Char × SubOpts)) (hid : 1 ≤ id ∧ id < 65536)
+    (hps : PropsBlockWF .subscribe ps) (hfs : fs ≠ [] ∧ FiltersWF fs) :
+    readSubscribeBody (printSubscribeBody id ps fs) = some (.subscribe id ps fs) := by
+  rw [readSubscribeBody_step,
+    show printSubscribeBody id ps fs
+      = writeBE 2 id ++ (printProps ps ++ printFilters fs) from rfl,
+    readNat_writeBE 2 id _ (by omega)]
+  simp only [Option.bind_some]
+  rw [if_pos (by omega : id ≠ 0), readProps_printProps .subscribe ps _ hps]
+  simp only [Option.bind_some]
+  rw [readFiltersGo_printFilters (printFilters fs).length fs
+    (printFilters_length_ge fs) hfs.2]
+  simp only [Option.bind_some]
+  have h2 : fs.isEmpty = false := by
+    cases fs with
+    | nil => exact absurd rfl hfs.1
+    | cons a t => rfl
+  rw [if_pos (by rw [h2]; rfl : ([].isEmpty && !fs.isEmpty) = true)]
+
+/-- Reason codes written as bytes read back as themselves. -/
+theorem map_toUInt8_toNat (rs : List Nat) (h : ∀ r ∈ rs, r < 256) :
+    (rs.map Nat.toUInt8).map UInt8.toNat = rs := by
+  induction rs with
+  | nil => rfl
+  | cons r rs' ih =>
+    simp only [List.map_cons]
+    rw [toNat_toUInt8 (h r (by simp)), ih (fun x hx => h x (by simp [hx]))]
+
+/-- The SUBACK body reader as one bind chain. -/
+theorem readSubackBody_step (seg : List UInt8) :
+    readSubackBody seg =
+    (readNat 2 seg).bind fun (id, r1) =>
+      if id ≠ 0 then
+        (readProps .suback r1).bind fun (props, r2) =>
+          if !r2.isEmpty then some (.suback id props (r2.map UInt8.toNat))
+          else none
+      else none := rfl
+
+/-- A printed SUBACK body reads back as the packet. -/
+theorem readSubackBody_printSubackBody (id : Nat) (ps : List Property)
+    (rs : List Nat) (hid : 1 ≤ id ∧ id < 65536)
+    (hps : PropsBlockWF .suback ps) (hrs : rs ≠ [] ∧ ∀ r ∈ rs, r < 256) :
+    readSubackBody (printSubackBody id ps rs) = some (.suback id ps rs) := by
+  rw [readSubackBody_step,
+    show printSubackBody id ps rs
+      = writeBE 2 id ++ (printProps ps ++ rs.map Nat.toUInt8) from rfl,
+    readNat_writeBE 2 id _ (by omega)]
+  simp only [Option.bind_some]
+  rw [if_pos (by omega : id ≠ 0), readProps_printProps .suback ps _ hps]
+  simp only [Option.bind_some]
+  have h2 : (rs.map Nat.toUInt8).isEmpty = false := by
+    cases rs with
+    | nil => exact absurd rfl hrs.1
+    | cons a t => rfl
+  rw [if_pos (by rw [h2]; rfl : (!(rs.map Nat.toUInt8).isEmpty) = true),
+    map_toUInt8_toNat rs hrs.2]
+
+/-- A printed DISCONNECT body reads back as the packet. -/
+theorem readDisconnectBody_print (x : Option (Nat × List Property))
+    (h : match x with
+      | none => True
+      | some (rc, ps) => rc < 256 ∧ PropsBlockWF PropSet.disconnect ps) :
+    readDisconnectBody (bodyOf (Packet.disconnect x))
+      = some (Packet.disconnect x) := by
+  cases x with
+  | none => rfl
+  | some rp =>
+    obtain ⟨rc, ps⟩ := rp
+    obtain ⟨hrc, hps⟩ := h
+    show readDisconnectBody ([rc.toUInt8] ++ printProps ps)
+        = some (Packet.disconnect (some (rc, ps)))
+    rw [show [rc.toUInt8] ++ printProps ps = rc.toUInt8 :: printProps ps from rfl]
+    have hpos : 0 < (printProps ps).length := by
+      show 0 < (printVBI (printPropsList ps).length
+        ++ printPropsList ps).length
+      rw [List.length_append]
+      have h1 := printVBI_pos (printPropsList ps).length
+      omega
+    have hne : ¬ ((printProps ps).isEmpty = true) := by
+      intro hcon
+      rw [List.isEmpty_iff] at hcon
+      have hz : (printProps ps).length = 0 := congrArg List.length hcon
+      omega
+    show (if (printProps ps).isEmpty
+        then some (Packet.disconnect (some ((rc.toUInt8).toNat, [])))
+        else (readProps PropSet.disconnect (printProps ps)).bind
+          fun (props, r2) =>
+          if r2.isEmpty
+            then some (Packet.disconnect (some ((rc.toUInt8).toNat, props)))
+            else none) = some (Packet.disconnect (some (rc, ps)))
+    rw [if_neg hne]
+    simp only [readProps_printProps_exact PropSet.disconnect ps hps,
+      Option.bind_some]
+    rw [if_pos (by decide : List.isEmpty [] = true), toNat_toUInt8 hrc]
+
+/-- The facts about a well formed connect flags byte: it
+    fits in a byte, the reserved bit is clear, and every field
+    the reader recovers from the byte (the will QoS, the will
+    retain, the will flag, the username and password flags,
+    the clean start) is the field that was written. -/
+theorem connectFlags_facts (c : Connect) (h : ConnectWF c) :
+    (connectFlags c).toUInt8.toNat = connectFlags c
+    ∧ connectFlags c % 2 = 0
+    ∧ (connectFlags c / 8) % 4
+        = (match c.will with | some w => w.qos | none => 0)
+    ∧ flagBit (connectFlags c) 7 = c.username.isSome
+    ∧ flagBit (connectFlags c) 6 = c.password.isSome
+    ∧ flagBit (connectFlags c) 5
+        = (match c.will with | some w => w.retain | none => false)
+    ∧ flagBit (connectFlags c) 2 = c.will.isSome
+    ∧ flagBit (connectFlags c) 1 = c.cleanStart := by
+  have e1 : (if c.username.isSome then (128 : Nat) else 0)
+      = (if c.username.isSome then 1 else 0) * 128 := if_bool_mul _ _
+  have e2 : (if c.password.isSome then (64 : Nat) else 0)
+      = (if c.password.isSome then 1 else 0) * 64 := if_bool_mul _ _
+  have e3 : (if c.cleanStart then (2 : Nat) else 0)
+      = (if c.cleanStart then 1 else 0) * 2 := if_bool_mul _ _
+  have hub : (if c.username.isSome then (1 : Nat) else 0) ≤ 1 := by
+    cases h : c.username.isSome <;> decide
+  have hpb : (if c.password.isSome then (1 : Nat) else 0) ≤ 1 := by
+    cases h : c.password.isSome <;> decide
+  have hcs : (if c.cleanStart then (1 : Nat) else 0) ≤ 1 := by
+    cases h : c.cleanStart <;> decide
+  cases hw : c.will with
+  | none =>
+    have hf : connectFlags c
+        = (if c.username.isSome then 1 else 0) * 128
+          + (if c.password.isSome then 1 else 0) * 64
+          + (if c.cleanStart then 1 else 0) * 2 := by
+      unfold connectFlags
+      rw [e1, e2, e3, hw]
+      dsimp only
+      omega
+    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+    · rw [hf]
+      exact toNat_toUInt8 (by omega)
+    · rw [hf]; omega
+    · show (connectFlags c / 8) % 4 = 0
+      rw [hf]; omega
+    · rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 7 = 128 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + (if c.cleanStart then 1 else 0) * 2) / 128 % 2
+          = (if c.username.isSome then 1 else 0) by omega]
+      cases h : c.username.isSome <;> rfl
+    · rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 6 = 64 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + (if c.cleanStart then 1 else 0) * 2) / 64 % 2
+          = (if c.password.isSome then 1 else 0) by omega]
+      cases h : c.password.isSome <;> rfl
+    · show flagBit (connectFlags c) 5 = false
+      rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 5 = 32 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + (if c.cleanStart then 1 else 0) * 2) / 32 % 2 = 0 by omega]
+      rfl
+    · show flagBit (connectFlags c) 2 = false
+      rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 2 = 4 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + (if c.cleanStart then 1 else 0) * 2) / 4 % 2 = 0 by omega]
+      rfl
+    · rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 1 = 2 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + (if c.cleanStart then 1 else 0) * 2) / 2 % 2
+          = (if c.cleanStart then 1 else 0) by omega]
+      cases h : c.cleanStart <;> rfl
+  | some w =>
+    have hwf : WillWF w := h.2.2.2.1 w hw
+    have hwq : w.qos ≤ 2 := hwf.1
+    have hrb : (if w.retain then (1 : Nat) else 0) ≤ 1 := by
+      cases w.retain <;> decide
+    have e4 : (if w.retain then (32 : Nat) else 0)
+        = (if w.retain then 1 else 0) * 32 := if_bool_mul _ _
+    have hf : connectFlags c
+        = (if c.username.isSome then 1 else 0) * 128
+          + (if c.password.isSome then 1 else 0) * 64
+          + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4)
+          + (if c.cleanStart then 1 else 0) * 2 := by
+      unfold connectFlags
+      rw [e1, e2, e3, hw]
+      dsimp only
+      rw [e4]
+    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+    · rw [hf]
+      exact toNat_toUInt8 (by omega)
+    · rw [hf]; omega
+    · show (connectFlags c / 8) % 4 = w.qos
+      rw [hf]; omega
+    · rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 7 = 128 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4)
+            + (if c.cleanStart then 1 else 0) * 2) / 128 % 2
+          = (if c.username.isSome then 1 else 0) by omega]
+      cases h : c.username.isSome <;> rfl
+    · rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 6 = 64 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4)
+            + (if c.cleanStart then 1 else 0) * 2) / 64 % 2
+          = (if c.password.isSome then 1 else 0) by omega]
+      cases h : c.password.isSome <;> rfl
+    · show flagBit (connectFlags c) 5 = w.retain
+      rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 5 = 32 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4)
+            + (if c.cleanStart then 1 else 0) * 2) / 32 % 2
+          = (if w.retain then 1 else 0) by omega]
+      cases w.retain <;> rfl
+    · show flagBit (connectFlags c) 2 = true
+      rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 2 = 4 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4)
+            + (if c.cleanStart then 1 else 0) * 2) / 4 % 2 = 1 by omega]
+      rfl
+    · rw [hf]
+      unfold flagBit
+      rw [show (2 : Nat) ^ 1 = 2 by decide,
+        show ((if c.username.isSome then 1 else 0) * 128
+            + (if c.password.isSome then 1 else 0) * 64
+            + ((if w.retain then 1 else 0) * 32 + w.qos * 8 + 4)
+            + (if c.cleanStart then 1 else 0) * 2) / 2 % 2
+          = (if c.cleanStart then 1 else 0) by omega]
+      cases h : c.cleanStart <;> rfl
+
+/-- The CONNECT tail: the optional username and password
+    fields read back as themselves, and nothing is left
+    over, so the assembled packet is the one that was
+    printed. The three flag values are the reader's own
+    recoveries from the flags byte; the hypotheses tie them
+    to the fields. -/
+theorem readOptFields (u : Option (List Char)) (p : Option (List UInt8))
+    (hu : ∀ s, u = some s → StrWF s) (hp : ∀ b, p = some b → BinWF b)
+    (cs : Bool) (ka : Nat) (props : List Property) (cid : List Char)
+    (will : Option Will) (f7 f6 f1 : Bool)
+    (h7 : f7 = u.isSome) (h6 : f6 = p.isSome) (h1 : f1 = cs) :
+    ((readOptStrField f7 (printOptStr u ++ printOptBin p)).bind
+        fun (u', r8) =>
+      (readOptBinField f6 r8).bind fun (p', r9) =>
+      (if r9.isEmpty
+        then some (⟨f1, ka, props, cid, will, u', p'⟩ : Connect) else none)
+      : Option Connect)
+    = some (⟨cs, ka, props, cid, will, u, p⟩ : Connect) := by
+  subst h7
+  subst h6
+  subst h1
+  cases u with
+  | none =>
+    rw [show printOptStr none = [] from rfl, List.nil_append]
+    unfold readOptStrField
+    rw [if_neg (by decide : ¬ (Option.isSome none = true))]
+    simp only [Option.bind_some]
+    cases p with
+    | none =>
+      rw [show printOptBin none = [] from rfl]
+      unfold readOptBinField
+      rw [if_neg (by decide : ¬ (Option.isSome none = true))]
+      simp only [Option.bind_some]
+      rw [if_pos (by decide : List.isEmpty [] = true)]
+    | some b =>
+      rw [show printOptBin (some b) = printBin b from rfl]
+      unfold readOptBinField
+      rw [if_pos (by rfl : Option.isSome (some b) = true),
+        ← List.append_nil (printBin b), readBin_printBin b [] (hp b rfl)]
+      simp only [Option.map_some, Option.bind_some]
+      rw [if_pos (by decide : List.isEmpty [] = true)]
+  | some s =>
+    rw [show printOptStr (some s) = printStr s from rfl]
+    unfold readOptStrField
+    rw [if_pos (by rfl : Option.isSome (some s) = true),
+      readStr_printStr s _ (hu s rfl)]
+    simp only [Option.map_some, Option.bind_some]
+    cases p with
+    | none =>
+      rw [show printOptBin none = [] from rfl]
+      unfold readOptBinField
+      rw [if_neg (by decide : ¬ (Option.isSome none = true))]
+      simp only [Option.bind_some]
+      rw [if_pos (by decide : List.isEmpty [] = true)]
+    | some b =>
+      rw [show printOptBin (some b) = printBin b from rfl]
+      unfold readOptBinField
+      rw [if_pos (by rfl : Option.isSome (some b) = true),
+        ← List.append_nil (printBin b), readBin_printBin b [] (hp b rfl)]
+      simp only [Option.map_some, Option.bind_some]
+      rw [if_pos (by decide : List.isEmpty [] = true)]
+
+/-- A printed CONNECT body reads back as the packet. -/
+theorem readConnectBody_printConnectBody (c : Connect) (h : ConnectWF c) :
+    readConnectBody (printConnectBody c) = some c := by
+  obtain ⟨hka, hprops, hcid, hwill, huser, hpass⟩ := h
+  obtain ⟨hf1, hf2, hf3, hf4, hf5, hf6, hf7, hf8⟩ := connectFlags_facts c
+    ⟨hka, hprops, hcid, hwill, huser, hpass⟩
+  have hfin : ∀ (w : Option Will), w = c.will →
+      (⟨c.cleanStart, c.keepAlive, c.props, c.clientId, w, c.username,
+        c.password⟩ : Connect) = c := by
+    intro w hw
+    subst hw
+    rfl
+  have hproto : StrWF ['M', 'Q', 'T', 'T'] := by
+    constructor
+    · decide
+    · decide
+  unfold readConnectBody
+  rw [show printConnectBody c
+      = printStr ['M', 'Q', 'T', 'T'] ++ ([5, (connectFlags c).toUInt8]
+        ++ (writeBE 2 c.keepAlive ++ (printProps c.props
+        ++ (printStr c.clientId ++ (printWillPart c.will
+        ++ (printOptStr c.username ++ printOptBin c.password))))))
+      from rfl,
+    readStr_printStr _ _ hproto]
+  simp only [Option.bind_some]
+  rw [if_pos trivial]
+  simp only [List.cons_append, List.nil_append]
+  rw [readByte_cons]
+  simp only [Option.bind_some]
+  rw [if_pos (by decide : (5 : UInt8).toNat = 5), readByte_cons]
+  simp only [Option.bind_some]
+  rw [hf1, if_pos hf2]
+  by_cases hwn : c.will = none
+  · have hf3' : (connectFlags c / 8) % 4 = 0 := by rw [hf3, hwn]
+    have hf7' : flagBit (connectFlags c) 2 = false := by simp [hf7, hwn]
+    rw [if_pos (by rw [hf3']; omega : (connectFlags c / 8) % 4 ≠ 3),
+      readNat_writeBE 2 c.keepAlive _ (by omega)]
+    simp only [Option.bind_some]
+    rw [readProps_printProps .connect c.props _ hprops]
+    simp only [Option.bind_some]
+    rw [readStr_printStr c.clientId _ hcid]
+    simp only [Option.bind_some]
+    rw [hwn, show printWillPart none = [] from rfl, List.nil_append]
+    unfold readWillPart
+    rw [if_neg (by rw [hf7']; decide : ¬ (flagBit (connectFlags c) 2 = true))]
+    simp only [Option.bind_some]
+    rw [readOptFields c.username c.password huser hpass c.cleanStart
+      c.keepAlive c.props c.clientId none (flagBit (connectFlags c) 7)
+      (flagBit (connectFlags c) 6) (flagBit (connectFlags c) 1) hf4 hf5 hf8]
+    exact congrArg Option.some (hfin none hwn.symm)
+  · obtain ⟨w, hw⟩ : ∃ w, c.will = some w := by
+      cases hw2 : c.will with
+      | none => exact absurd hw2 hwn
+      | some w => exact ⟨w, rfl⟩
+    obtain ⟨wq, wr, wps, wt, wpay⟩ := w
+    have hwf : WillWF ⟨wq, wr, wps, wt, wpay⟩ := hwill _ hw
+    have hwq : wq ≤ 2 := hwf.1
+    have hwprops : PropsBlockWF .will wps := hwf.2.1
+    have hwtopic : TopicWF wt := hwf.2.2.1
+    have hwpay : BinWF wpay := hwf.2.2.2
+    have hf3' : (connectFlags c / 8) % 4 = wq := by rw [hf3, hw]
+    have hf6' : flagBit (connectFlags c) 5 = wr := by rw [hf6, hw]
+    have hf7' : flagBit (connectFlags c) 2 = true := by simp [hf7, hw]
+    rw [if_pos (by rw [hf3']; omega : (connectFlags c / 8) % 4 ≠ 3),
+      readNat_writeBE 2 c.keepAlive _ (by omega)]
+    simp only [Option.bind_some]
+    rw [readProps_printProps .connect c.props _ hprops]
+    simp only [Option.bind_some]
+    rw [readStr_printStr c.clientId _ hcid]
+    simp only [Option.bind_some]
+    rw [hw, show printWillPart (some ⟨wq, wr, wps, wt, wpay⟩)
+        = printProps wps ++ (printStr wt ++ printBin wpay) from rfl]
+    unfold readWillPart
+    rw [if_pos hf7', List.append_assoc, readProps_printProps .will wps _ hwprops]
+    simp only [Option.bind_some]
+    rw [List.append_assoc, readStr_printStr wt _ hwtopic.1]
+    simp only [Option.bind_some]
+    rw [checkTopic_of_wf hwtopic]
+    simp only [Option.bind_some]
+    rw [readBin_printBin wpay _ hwpay]
+    simp only [Option.bind_some]
+    rw [readOptFields c.username c.password huser hpass c.cleanStart
+      c.keepAlive c.props c.clientId
+      (some ⟨(connectFlags c / 8) % 4, flagBit (connectFlags c) 5, wps, wt,
+        wpay⟩)
+      (flagBit (connectFlags c) 7) (flagBit (connectFlags c) 6)
+      (flagBit (connectFlags c) 1) hf4 hf5 hf8]
+    rw [hf3', hf6']
+    exact congrArg Option.some (hfin _ hw.symm)
+
+/-- The packet identifier step at QoS 0 reads nothing. -/
+theorem readPacketId_qos0 (flags : Nat) (r : List UInt8)
+    (h : (flags / 2) % 4 = 0) :
+    readPacketId flags r = some (none, r) := by
+  unfold readPacketId
+  rw [if_pos h]
+
+/-- The packet identifier step at QoS 1 and 2 reads a printed
+    nonzero identifier. -/
+theorem readPacketId_print (flags : Nat) (i : Nat) (rest : List UInt8)
+    (h : (flags / 2) % 4 ≠ 0) (hi : 1 ≤ i ∧ i < 65536) :
+    readPacketId flags (printIdOpt (some i) ++ rest) = some (some i, rest) := by
+  unfold readPacketId
+  rw [if_neg h, show printIdOpt (some i) = writeBE 2 i from rfl,
+    readNat_writeBE 2 i _ (by omega)]
+  simp only [Option.bind_some]
+  rw [if_pos (by omega : i ≠ 0)]
+
+/-- A printed PUBLISH body reads back as the packet, when the
+    flags word carries the packet's own QoS, DUP and RETAIN. -/
+theorem readPublishBody_printPublishBody (flags : Nat) (pub : Publish)
+    (hq : (flags / 2) % 4 = pub.qos) (h3 : flagBit flags 3 = pub.dup)
+    (h0 : flagBit flags 0 = pub.retain) (h : PublishWF pub) :
+    readPublishBody flags (printPublishBody pub) = some pub := by
+  obtain ⟨dup, qos, retain, topic, pid, props, payload⟩ := pub
+  obtain ⟨hqos, htopic, hidf, hnone, hprops⟩ := h
+  have htopic' : TopicWF topic := htopic
+  have hidf' : ∀ id, pid = some id →
+      1 ≤ id ∧ id < 65536 ∧ (qos = 1 ∨ qos = 2) := hidf
+  have hnone' : pid = none → qos = 0 := hnone
+  have hprops' : PropsBlockWF .publish props := hprops
+  have hq' : (flags / 2) % 4 = qos := hq
+  have h3' : flagBit flags 3 = dup := h3
+  have h0' : flagBit flags 0 = retain := h0
+  unfold readPublishBody
+  rw [show printPublishBody ⟨dup, qos, retain, topic, pid, props, payload⟩
+      = printStr topic ++ (printIdOpt pid ++ (printProps props ++ payload))
+      from rfl,
+    readStr_printStr topic _ htopic'.1]
+  simp only [Option.bind_some]
+  rw [checkTopic_of_wf htopic']
+  simp only [Option.bind_some]
+  by_cases hq0 : qos = 0
+  · have hpid : pid = none := by
+      cases hp : pid with
+      | none => rfl
+      | some i =>
+        have h2 := hidf' i hp
+        omega
+    rw [hpid, show printIdOpt none = [] from rfl, List.nil_append,
+      readPacketId_qos0 flags _ (by omega)]
+    simp only [Option.bind_some]
+    rw [readProps_printProps .publish props payload hprops']
+    simp only [Option.bind_some]
+    rw [h3', h0', hq']
+  · have hpid : ∃ i, pid = some i ∧ 1 ≤ i ∧ i < 65536 := by
+      cases hp : pid with
+      | none => exact absurd (hnone' hp) hq0
+      | some i =>
+        have h2 := hidf' i hp
+        exact ⟨i, rfl, h2.1, h2.2.1⟩
+    obtain ⟨i, hi, hi1, hi2⟩ := hpid
+    rw [hi, readPacketId_print flags i _ (by omega) ⟨hi1, hi2⟩]
+    simp only [Option.bind_some]
+    rw [readProps_printProps .publish props payload hprops']
+    simp only [Option.bind_some]
+    rw [h3', h0', hq']
+
+/-! ## Whole packets -/
+
+/-- A well formed PUBLISH header byte value fits in a
+    byte: the fixed part is 0x30 and the flags part is at
+    most 8 + 4 + 1. -/
+theorem publishHeader_bound (pub : Publish) (h : PublishWF pub) :
+    publishHeader pub < 256 := by
+  have hA : (if pub.dup then (8 : Nat) else 0) ≤ 8 := by
+    cases pub.dup <;> decide
+  have hB : (if pub.retain then (1 : Nat) else 0) ≤ 1 := by
+    cases pub.retain <;> decide
+  have hqos : pub.qos ≤ 2 := h.1
+  unfold publishHeader
+  omega
+
+/-- The body dispatcher on a printed CONNECT body. -/
+theorem parseBody_connect (c : Connect) (h : ConnectWF c) :
+    parseBody 1 0 (printConnectBody c) = some (.connect c) := by
+  show (readConnectBody (printConnectBody c)).map Packet.connect
+    = some (.connect c)
+  rw [readConnectBody_printConnectBody c h]
+  simp only [Option.map_some]
+
+/-- The body dispatcher on a printed PUBLISH body. -/
+theorem parseBody_publish (pub : Publish) (h : PublishWF pub) :
+    parseBody 3 (publishHeader pub % 16) (printPublishBody pub)
+      = some (.publish pub) := by
+  have hqos : pub.qos ≤ 2 := h.1
+  have hA : (if pub.dup then (8 : Nat) else 0) ≤ 8 := by
+    cases pub.dup <;> decide
+  have hB : (if pub.retain then (1 : Nat) else 0) ≤ 1 := by
+    cases pub.retain <;> decide
+  have hE : (if pub.dup then 8 else 0) + pub.qos * 2
+      + (if pub.retain then 1 else 0) ≤ 15 := by omega
+  have hphv : publishHeader pub
+      = 48 + ((if pub.dup then 8 else 0) + pub.qos * 2
+        + (if pub.retain then 1 else 0)) := by
+    unfold publishHeader
+    omega
+  have hmod : publishHeader pub % 16
+      = (if pub.dup then 8 else 0) + pub.qos * 2
+        + (if pub.retain then 1 else 0) := by omega
+  have hb := publish_bits pub.dup pub.retain pub.qos hqos
+  show (if (publishHeader pub % 16 / 2) % 4 = 3 then none
+    else (readPublishBody (publishHeader pub % 16) (printPublishBody pub)).map
+      Packet.publish) = some (.publish pub)
+  rw [hmod, if_neg (by rw [hb.1]; omega :
+      ¬ ((if pub.dup then 8 else 0) + pub.qos * 2
+        + (if pub.retain then 1 else 0)) / 2 % 4 = 3),
+    readPublishBody_printPublishBody _ pub hb.1 hb.2.1 hb.2.2 h]
+  simp only [Option.map_some]
+
+/-- The body dispatcher on a printed SUBSCRIBE body. -/
+theorem parseBody_subscribe (id : Nat) (ps : List Property)
+    (fs : List (List Char × SubOpts)) (hid : 1 ≤ id ∧ id < 65536)
+    (hps : PropsBlockWF .subscribe ps) (hfs : fs ≠ [] ∧ FiltersWF fs) :
+    parseBody 8 2 (printSubscribeBody id ps fs)
+      = some (.subscribe id ps fs) := by
+  show (if (2 : Nat) = 2 then readSubscribeBody (printSubscribeBody id ps fs)
+    else none) = some (.subscribe id ps fs)
+  rw [if_pos rfl, readSubscribeBody_printSubscribeBody id ps fs hid hps hfs]
+
+/-- The body dispatcher on a printed SUBACK body. -/
+theorem parseBody_suback (id : Nat) (ps : List Property) (rs : List Nat)
+    (hid : 1 ≤ id ∧ id < 65536) (hps : PropsBlockWF .suback ps)
+    (hrs : rs ≠ [] ∧ ∀ r ∈ rs, r < 256) :
+    parseBody 9 0 (printSubackBody id ps rs) = some (.suback id ps rs) := by
+  show (if (0 : Nat) = 0 then readSubackBody (printSubackBody id ps rs)
+    else none) = some (.suback id ps rs)
+  rw [if_pos rfl, readSubackBody_printSubackBody id ps rs hid hps hrs]
+
+/-- The body dispatcher on an empty PINGREQ body: a closed
+    computation. -/
+theorem parseBody_pingreq : parseBody 12 0 [] = some .pingreq := by decide
+
+/-- The body dispatcher on an empty PINGRESP body. -/
+theorem parseBody_pingresp : parseBody 13 0 [] = some .pingresp := by decide
+
+/-- The body dispatcher on an empty DISCONNECT body. -/
+theorem parseBody_disconnect_none :
+    parseBody 14 0 (bodyOf (.disconnect none)) = some (.disconnect none) := by
+  show (if (0 : Nat) = 0 then readDisconnectBody (bodyOf (.disconnect none))
+    else none) = some (.disconnect none)
+  rw [if_pos rfl, readDisconnectBody_print none trivial]
+
+/-- The body dispatcher on a printed DISCONNECT body with a
+    reason code and properties. -/
+theorem parseBody_disconnect_some (rc : Nat) (ps : List Property)
+    (h : rc < 256 ∧ PropsBlockWF PropSet.disconnect ps) :
+    parseBody 14 0 (bodyOf (.disconnect (some (rc, ps))))
+      = some (.disconnect (some (rc, ps))) := by
+  show (if (0 : Nat) = 0
+      then readDisconnectBody (bodyOf (.disconnect (some (rc, ps))))
+      else none) = some (.disconnect (some (rc, ps)))
+  rw [if_pos rfl, readDisconnectBody_print (some (rc, ps)) h]
+
+/-- One packet at the head of a stream: a printed packet
+    followed by any bytes parses to the packet and leaves
+    the rest of the stream untouched. -/
+theorem parsePacket_print (p : Packet) (rest : List UInt8) (h : PacketWF p) :
+    parsePacket (print p ++ rest) = some (p, rest) := by
+  obtain ⟨hfields, hlen⟩ := h
+  have hnorm : print p ++ rest
+      = headerOf p :: (printVBI (bodyOf p).length ++ (bodyOf p ++ rest)) := by
+    show (headerOf p :: (printVBI (bodyOf p).length ++ bodyOf p)) ++ rest
+      = headerOf p :: (printVBI (bodyOf p).length ++ (bodyOf p ++ rest))
+    rw [List.cons_append, List.append_assoc]
+  rw [hnorm]
+  show ((decVBI (printVBI (bodyOf p).length ++ (bodyOf p ++ rest))).bind
+      fun (len, r1) =>
+    (readBytes len r1).bind fun (seg, r2) =>
+    (parseBody ((headerOf p).toNat / 16) ((headerOf p).toNat % 16) seg).bind
+      fun q => some (q, r2)) = some (p, rest)
+  rw [decVBI_printVBI _ _ hlen]
+  simp only [Option.bind_some]
+  rw [readBytes_append _ _ _ rfl]
+  simp only [Option.bind_some]
+  cases p with
+  | connect c =>
+    have hfc : ConnectWF c := hfields
+    have e1 : (headerOf (.connect c)).toNat / 16 = 1 := by
+      rw [show headerOf (.connect c) = (0x10 : UInt8) from rfl]; decide
+    have e2 : (headerOf (.connect c)).toNat % 16 = 0 := by
+      rw [show headerOf (.connect c) = (0x10 : UInt8) from rfl]; decide
+    have e3 : bodyOf (.connect c) = printConnectBody c := rfl
+    rw [e1, e2, e3]
+    simp only [parseBody_connect c hfc, Option.bind_some]
+  | publish pub =>
+    have hfp : PublishWF pub := hfields
+    have hph : (publishHeader pub).toUInt8.toNat = publishHeader pub :=
+      toNat_toUInt8 (publishHeader_bound pub hfp)
+    have hqos : pub.qos ≤ 2 := hfp.1
+    have hA : (if pub.dup then (8 : Nat) else 0) ≤ 8 := by
+      cases pub.dup <;> decide
+    have hB : (if pub.retain then (1 : Nat) else 0) ≤ 1 := by
+      cases pub.retain <;> decide
+    have hphv : publishHeader pub
+        = 48 + ((if pub.dup then 8 else 0) + pub.qos * 2
+          + (if pub.retain then 1 else 0)) := by
+      unfold publishHeader
+      omega
+    have hE : (if pub.dup then 8 else 0) + pub.qos * 2
+        + (if pub.retain then 1 else 0) ≤ 15 := by omega
+    have hdiv : publishHeader pub / 16 = 3 := by omega
+    have e3 : bodyOf (.publish pub) = printPublishBody pub := rfl
+    have e0 : headerOf (.publish pub) = (publishHeader pub).toUInt8 := rfl
+    rw [e3, e0, hph, hdiv]
+    simp only [parseBody_publish pub hfp, Option.bind_some]
+  | subscribe id ps fs =>
+    have hid : 1 ≤ id ∧ id < 65536 := ⟨hfields.1, hfields.2.1⟩
+    have hps : PropsBlockWF .subscribe ps := hfields.2.2.1
+    have hfs : fs ≠ [] ∧ FiltersWF fs := ⟨hfields.2.2.2.1, hfields.2.2.2.2⟩
+    have e1 : (headerOf (.subscribe id ps fs)).toNat / 16 = 8 := by
+      rw [show headerOf (.subscribe id ps fs) = (0x82 : UInt8) from rfl]; decide
+    have e2 : (headerOf (.subscribe id ps fs)).toNat % 16 = 2 := by
+      rw [show headerOf (.subscribe id ps fs) = (0x82 : UInt8) from rfl]; decide
+    have e3 : bodyOf (.subscribe id ps fs) = printSubscribeBody id ps fs := rfl
+    rw [e1, e2, e3]
+    simp only [parseBody_subscribe id ps fs hid hps hfs, Option.bind_some]
+  | suback id ps rs =>
+    have hid : 1 ≤ id ∧ id < 65536 := ⟨hfields.1, hfields.2.1⟩
+    have hps : PropsBlockWF .suback ps := hfields.2.2.1
+    have hrs : rs ≠ [] ∧ ∀ r ∈ rs, r < 256 :=
+      ⟨hfields.2.2.2.1, hfields.2.2.2.2⟩
+    have e1 : (headerOf (.suback id ps rs)).toNat / 16 = 9 := by
+      rw [show headerOf (.suback id ps rs) = (0x90 : UInt8) from rfl]; decide
+    have e2 : (headerOf (.suback id ps rs)).toNat % 16 = 0 := by
+      rw [show headerOf (.suback id ps rs) = (0x90 : UInt8) from rfl]; decide
+    have e3 : bodyOf (.suback id ps rs) = printSubackBody id ps rs := rfl
+    rw [e1, e2, e3]
+    simp only [parseBody_suback id ps rs hid hps hrs, Option.bind_some]
+  | pingreq =>
+    have e1 : (headerOf .pingreq).toNat / 16 = 12 := by decide
+    have e2 : (headerOf .pingreq).toNat % 16 = 0 := by decide
+    have e3 : bodyOf .pingreq = [] := rfl
+    rw [e1, e2, e3]
+    simp only [parseBody_pingreq, Option.bind_some]
+  | pingresp =>
+    have e1 : (headerOf .pingresp).toNat / 16 = 13 := by decide
+    have e2 : (headerOf .pingresp).toNat % 16 = 0 := by decide
+    have e3 : bodyOf .pingresp = [] := rfl
+    rw [e1, e2, e3]
+    simp only [parseBody_pingresp, Option.bind_some]
+  | disconnect x =>
+    have e1 : (headerOf (.disconnect x)).toNat / 16 = 14 := by
+      rw [show headerOf (.disconnect x) = (0xE0 : UInt8) from rfl]; decide
+    have e2 : (headerOf (.disconnect x)).toNat % 16 = 0 := by
+      rw [show headerOf (.disconnect x) = (0xE0 : UInt8) from rfl]; decide
+    rw [e1, e2]
+    cases x with
+    | none =>
+      simp only [parseBody_disconnect_none, Option.bind_some]
+    | some rp =>
+      obtain ⟨rc, ps⟩ := rp
+      have h2 : rc < 256 ∧ PropsBlockWF PropSet.disconnect ps := hfields
+      simp only [parseBody_disconnect_some rc ps h2, Option.bind_some]
+
+/-- The main round trip claim: a well formed packet,
+    printed and parsed back on its own, is the same
+    packet. -/
+theorem parse_print (p : Packet) (h : PacketWF p) : parse (print p) = some p := by
+  unfold parse
+  have h2 := parsePacket_print p [] h
+  rw [List.append_nil] at h2
+  simp only [h2]
+
+end Mqtt.Proofs
diff --git a/Proofs/SpecProofs.lean b/Proofs/SpecProofs.lean
new file mode 100644
index 0000000..77d2d1b
--- /dev/null
+++ b/Proofs/SpecProofs.lean
@@ -0,0 +1,91 @@
+/-
+  Proofs of the statements in `Spec.lean`, under the same names.
+
+  The round trips are the theorems proved in
+  `Proofs/RoundTrip.lean`. The refusals are single inputs,
+  checked in the kernel with `decide +kernel`: no native
+  evaluation, which the bar forbids.
+-/
+
+import Mqtt
+import Proofs.RoundTrip
+
+open Mqtt
+
+theorem Spec.parsePacket_print (p : Packet) (rest : List UInt8)
+    (h : PacketWF p) :
+    parsePacket (print p ++ rest) = some (p, rest) :=
+  Mqtt.Proofs.parsePacket_print p rest h
+
+theorem Spec.parse_print (p : Packet) (h : PacketWF p) :
+    parse (print p) = some p :=
+  Mqtt.Proofs.parse_print p h
+
+theorem Spec.decVBI_printVBI (n : Nat) (rest : List UInt8)
+    (hn : n < 268435456) :
+    decVBI (printVBI n ++ rest) = some (n, rest) :=
+  Mqtt.Proofs.decVBI_printVBI n rest hn
+
+
+theorem Spec.rejects_five_byte_remaining_length :
+    (parse ([192, 255, 255, 255, 255, 127] : List UInt8)).isSome
+      = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_subscribe_flags :
+    (parse ([128, 7, 0, 1, 0, 0, 1, 97, 0] : List UInt8)).isSome
+      = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_publish_qos3 :
+    (parse ([54, 7, 0, 1, 97, 0, 1, 0, 120] : List UInt8)).isSome
+      = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_wildcard_topic :
+    (parse ([48, 7, 0, 3, 97, 47, 35, 0, 120] : List UInt8)).isSome
+      = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_wrong_protocol_name :
+    (parse ([16, 14, 0, 4, 77, 81, 84, 85, 5, 2, 0, 0, 0, 0, 1, 120]
+      : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_reserved_connect_flag :
+    (parse ([16, 14, 0, 4, 77, 81, 84, 84, 5, 3, 0, 0, 0, 0, 1, 120]
+      : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_property_wrong_type :
+    (parse ([16, 16, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 2, 11, 5, 0,
+      1, 120] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_repeated_property :
+    (parse ([50, 12, 0, 1, 97, 0, 3, 6, 35, 0, 1, 35, 0, 2]
+      : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_subscribe_id_zero :
+    (parse ([130, 7, 0, 0, 0, 0, 1, 97, 0] : List UInt8)).isSome
+      = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_pingreq_body :
+    (parse ([192, 1, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_unknown_type :
+    (parse ([32, 0] : List UInt8)).isSome = false := by
+  decide +kernel
diff --git a/Proofs/Utf8.lean b/Proofs/Utf8.lean
new file mode 100644
index 0000000..6fe01b2
--- /dev/null
+++ b/Proofs/Utf8.lean
@@ -0,0 +1,148 @@
+/-
+  Proofs for the strict UTF-8 codec in Mqtt/Utf8.lean: the one
+  claim the packet round trip needs is that decoding the
+  encoding of any text gives the text back.
+
+  Carried in with the codec from the Proven Commons jws slice,
+  where this proof was first written, and adapted to the
+  renamed namespace.
+-/
+
+import Mqtt.Utf8
+
+namespace Mqtt.Utf8.Proofs
+
+open Mqtt.Utf8
+
+/-- A number below 256 written as a byte reads back as itself. -/
+theorem toNat_toUInt8 {k : Nat} (h : k < 256) : k.toUInt8.toNat = k := by
+  simp; omega
+
+/-- A character value is below 110000, and no character value
+    lies in the surrogate gap D800 to DFFF: the Unicode scalar
+    range every `Char` lives in. -/
+theorem char_bounds (c : Char) :
+    c.toNat < 0x110000 ∧ ¬ (0xD800 ≤ c.toNat ∧ c.toNat < 0xE000) := by
+  have h := c.valid
+  show c.val.toNat < 0x110000 ∧ ¬ (0xD800 ≤ c.val.toNat ∧ c.val.toNat < 0xE000)
+  rcases h with h | ⟨h1, h2⟩
+  · exact ⟨by omega, by omega⟩
+  · exact ⟨by omega, by omega⟩
+
+/-- A byte whose value is known to be a continuation byte reads
+    back as its payload value. -/
+theorem contVal_of_toNat {b : UInt8} {k : Nat} (h : b.toNat = 0x80 + k) (hk : k < 64) :
+    contVal b = some k := by
+  unfold contVal
+  rw [h, if_pos ⟨by omega, by omega⟩, Nat.add_sub_cancel_left]
+
+/-- One step of the decoder on a plain byte. -/
+theorem decode_one (b : UInt8) (bs : List UInt8) (hb : b.toNat < 0x80) :
+    decode (b :: bs) = (decode bs).map (Char.ofNat b.toNat :: ·) := by
+  cases bs with
+  | nil => rw [decode.eq_3, if_pos hb]
+  | cons b1 bs' => rw [decode.eq_2, if_pos hb]
+
+/-- One step of the decoder on a two byte form. -/
+theorem decode_two (b b1 : UInt8) (bs : List UInt8) (v : Nat)
+    (hb : 0xC2 ≤ b.toNat ∧ b.toNat < 0xE0) (hv : contVal b1 = some v) :
+    decode (b :: b1 :: bs) =
+      (decode bs).map (Char.ofNat ((b.toNat - 0xC0) * 64 + v) :: ·) := by
+  rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80),
+    if_neg (by omega : ¬ b.toNat < 0xC2), if_pos (by omega : b.toNat < 0xE0), hv]
+
+/-- One step of the decoder on a three byte form. -/
+theorem decode_three (b b1 b2 : UInt8) (bs : List UInt8) (v1 v2 : Nat)
+    (hb : 0xE0 ≤ b.toNat ∧ b.toNat < 0xF0)
+    (hside : (b.toNat = 0xE0 → 0x20 ≤ v1) ∧ (b.toNat = 0xED → v1 < 0x20))
+    (hv1 : contVal b1 = some v1) (hv2 : contVal b2 = some v2) :
+    decode (b :: b1 :: b2 :: bs) =
+      (decode bs).map (Char.ofNat ((b.toNat - 0xE0) * 4096 + v1 * 64 + v2) :: ·) := by
+  rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80),
+    if_neg (by omega : ¬ b.toNat < 0xC2), if_neg (by omega : ¬ b.toNat < 0xE0),
+    if_pos (by omega : b.toNat < 0xF0)]
+  dsimp only
+  rw [hv1, hv2]
+  dsimp only
+  rw [if_pos hside]
+
+/-- One step of the decoder on a four byte form. -/
+theorem decode_four (b b1 b2 b3 : UInt8) (bs : List UInt8) (v1 v2 v3 : Nat)
+    (hb : 0xF0 ≤ b.toNat ∧ b.toNat < 0xF5)
+    (hside : (b.toNat = 0xF0 → 0x10 ≤ v1) ∧ (b.toNat = 0xF4 → v1 < 0x10))
+    (hv1 : contVal b1 = some v1) (hv2 : contVal b2 = some v2)
+    (hv3 : contVal b3 = some v3) :
+    decode (b :: b1 :: b2 :: b3 :: bs) =
+      (decode bs).map
+        (Char.ofNat ((b.toNat - 0xF0) * 262144 + v1 * 4096 + v2 * 64 + v3) :: ·) := by
+  rw [decode.eq_2, if_neg (by omega : ¬ b.toNat < 0x80),
+    if_neg (by omega : ¬ b.toNat < 0xC2), if_neg (by omega : ¬ b.toNat < 0xE0),
+    if_neg (by omega : ¬ b.toNat < 0xF0), if_pos (by omega : b.toNat < 0xF5)]
+  dsimp only
+  rw [hv1, hv2, hv3]
+  dsimp only
+  rw [if_pos hside]
+
+/-- Decoding one encoded character in front of any bytes decodes
+    the character and then the bytes. The four cases are the
+    four lengths; each one applies the step lemma for its
+    length, checks the side conditions with arithmetic, and
+    rebuilds the character value. -/
+theorem decode_append_char (c : Char) (bs : List UInt8) :
+    decode (encodeChar c ++ bs) = (decode bs).map (c :: ·) := by
+  obtain ⟨hmax, hnsur⟩ := char_bounds c
+  by_cases h1 : c.toNat < 0x80
+  · rw [encodeChar, if_pos h1, List.cons_append, List.nil_append,
+      decode_one _ _ (by rw [toNat_toUInt8 (by omega)]; exact h1),
+      toNat_toUInt8 (by omega), Char.ofNat_toNat]
+  · rw [encodeChar, if_neg h1]
+    by_cases h2 : c.toNat < 0x800
+    · have hlead : (0xC0 + c.toNat / 64).toUInt8.toNat = 0xC0 + c.toNat / 64 :=
+        toNat_toUInt8 (by omega)
+      rw [if_pos h2, List.cons_append, List.cons_append, List.nil_append,
+        decode_two _ _ _ _ ⟨by omega, by omega⟩
+          (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))),
+        hlead,
+        show (0xC0 + c.toNat / 64 - 0xC0) * 64 + c.toNat % 64 = c.toNat by omega,
+        Char.ofNat_toNat]
+    · rw [if_neg h2]
+      by_cases h3 : c.toNat < 0x10000
+      · have hlead : (0xE0 + c.toNat / 4096).toUInt8.toNat = 0xE0 + c.toNat / 4096 :=
+          toNat_toUInt8 (by omega)
+        rw [if_pos h3, List.cons_append, List.cons_append, List.cons_append,
+          List.nil_append,
+          decode_three _ _ _ _ _ _ ⟨by omega, by omega⟩
+            ⟨fun hb => by rw [hlead] at hb; omega,
+             fun hb => by rw [hlead] at hb; omega⟩
+            (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide)))
+            (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))),
+          hlead,
+          show (0xE0 + c.toNat / 4096 - 0xE0) * 4096 + (c.toNat / 64) % 64 * 64 +
+            c.toNat % 64 = c.toNat by omega,
+          Char.ofNat_toNat]
+      · have hlead : (0xF0 + c.toNat / 262144).toUInt8.toNat = 0xF0 + c.toNat / 262144 :=
+          toNat_toUInt8 (by omega)
+        rw [if_neg h3, List.cons_append, List.cons_append, List.cons_append,
+          List.cons_append, List.nil_append,
+          decode_four _ _ _ _ _ _ _ _ ⟨by omega, by omega⟩
+            ⟨fun hb => by rw [hlead] at hb; omega,
+             fun hb => by rw [hlead] at hb; omega⟩
+            (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide)))
+            (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide)))
+            (contVal_of_toNat (toNat_toUInt8 (by omega)) (Nat.mod_lt _ (by decide))),
+          hlead,
+          show (0xF0 + c.toNat / 262144 - 0xF0) * 262144 + (c.toNat / 4096) % 64 * 4096 +
+            (c.toNat / 64) % 64 * 64 + c.toNat % 64 = c.toNat by omega,
+          Char.ofNat_toNat]
+
+/-- Decoding the encoding of any text gives the text back. -/
+theorem decode_encode : ∀ cs : List Char, decode (encode cs) = some cs := by
+  intro cs
+  induction cs with
+  | nil => rfl
+  | cons c cs ih =>
+    show decode (encodeChar c ++ encode cs) = some (c :: cs)
+    rw [decode_append_char, ih]
+    rfl
+
+end Mqtt.Utf8.Proofs
diff --git a/README.md b/README.md
index 6d3fa52..a94ed12 100644
--- a/README.md
+++ b/README.md
@@ -1,35 +1,200 @@
-# mqtt
+# mqtt: an MQTT 5.0 packet reader and printer, with a proved round trip
 
-A Lean parser for MQTT 5.0 packet framing. This is a Proven Commons project: it rebuilds a widely used format in Lean and proves the new code follows its written specification.
+Status: in-progress
 
-Status: not verified. No code has landed yet. Plan issue 1 holds the first slice, and it is unclaimed. The specification has not been approved by a reviewer, so do not call this verified.
+An MQTT 5.0 control packet reader and printer in Lean,
+covering the seven packet types CONNECT, PUBLISH, SUBSCRIBE,
+SUBACK, PINGREQ, PINGRESP, and DISCONNECT, with their
+property blocks. The reader reads one packet from the front
+of a byte list and returns the rest of the input, so a
+caller can walk a stream of packets. The definitions are in
+`Mqtt/Value.lean` (the packet types, the property table,
+the printer, and the well-formedness rules), `Mqtt/Parse.lean`
+(the reader), and `Mqtt/Utf8.lean` (a strict UTF-8 codec,
+carried in from the Proven Commons `jws` slice with its
+namespace renamed, as the header of that file records). The
+rules are written out in `SPEC.md`. This slice is framing
+only: no broker, no client, and no session behaviour.
 
-## First slice
+The statements a reviewer approves are in `Spec.lean`,
+with their proofs in `Proofs/SpecProofs.lean`. No reviewer
+has approved them yet, so this project is not called
+verified.
 
-MQTT 5.0 packets over TCP. Fixed header, remaining length as a variable byte integer capped at four bytes, and packet types CONNECT, PUBLISH, SUBSCRIBE, SUBACK, PINGREQ, PINGRESP, and DISCONNECT first. Properties are parsed per packet type. A property on a packet type that does not allow it is rejected.
+## How to run it
 
-This is distinct from the websocket repo. MQTT can run over websockets as a transport, but this slice is MQTT packets over TCP, not websocket frames.
+`lake build` builds the library, the proofs, and the
+command line tool. The tool reads one request per line:
+the word `parse`, a space, and the packet as
+comma-separated decimal byte codes. It answers `ok:` and
+the byte codes of the canonical reprint when the bytes are
+one packet, `none` when they are rejected, and `error` when
+the request itself is malformed.
 
-## Main claim
+```
+lake build
+echo "parse 192,0" | .lake/build/bin/mqtt
+```
 
-Decoding an encoding gives the same packet back. The decoder returns an error instead of reading past the end of its input. A variable byte integer longer than four bytes is rejected.
+That request is a PINGREQ, and the answer is `ok:192,0`: the
+packet read back and reprinted. A PINGREQ carrying a body
+(`parse 192,1,0`) answers `none`. See `SPEC.md` for the full
+protocol.
 
-## Test oracles
+`python3 tests/run_tests.py` rebuilds the tool, runs the
+fixed cases, the differential run against the harness
+oracle, the Paho cross-check when the library is
+importable, and the mutation and rejection cases, and
+writes the outcome to `tests/TEST-RESULTS.md`.
 
-- Eclipse Paho clients.
-- The Mosquitto broker test suite.
-- MQTT 5.0 specification test material.
+## What is proved
 
-## Score
+Each claim below names the theorem behind it. The
+theorems are stated in `Spec.lean` (the challenge file,
+where they end in `sorry`) and proved in
+`Proofs/SpecProofs.lean`, under the same names.
+`comparator.json` lists all of them.
 
-16 out of 18, first pass score in mission issue 19, the round 4 sheet. Created at the org owner's direction on that sheet, on the judgement that the slice, claim, and oracles are sound and that it duplicates no existing repo.
+| Claim | Theorem |
+|-------|---------|
+| Parsing the printed form of a well formed packet, with more stream bytes after it, gives the packet and those bytes back. | `Spec.parsePacket_print` |
+| Parsing the printed form of a well formed packet on its own gives the packet back. | `Spec.parse_print` |
+| Reading a printed variable byte integer gives the number back, for every value below 2^28. | `Spec.decVBI_printVBI` |
+| A remaining length whose fourth byte carries a continuation mark, so the value would need a fifth byte, is refused. | `Spec.rejects_five_byte_remaining_length` |
+| A SUBSCRIBE packet with flags 0000 is refused: the value the standard fixes is 0010. | `Spec.rejects_subscribe_flags` |
+| A PUBLISH packet with the reserved QoS value 3 is refused. | `Spec.rejects_publish_qos3` |
+| A PUBLISH topic name holding a wildcard is refused. | `Spec.rejects_wildcard_topic` |
+| A CONNECT whose protocol name is not `MQTT` is refused. | `Spec.rejects_wrong_protocol_name` |
+| A CONNECT with the reserved bit of the connect flags byte set is refused. | `Spec.rejects_reserved_connect_flag` |
+| A property standing on a packet type that does not allow it, here a subscription identifier on a CONNECT, is refused. | `Spec.rejects_property_wrong_type` |
+| A single use property standing twice in one block, here the topic alias on a PUBLISH, is refused. | `Spec.rejects_repeated_property` |
+| A SUBSCRIBE with packet identifier 0 is refused. | `Spec.rejects_subscribe_id_zero` |
+| A PINGREQ with a body is refused: its remaining length must be 0. | `Spec.rejects_pingreq_body` |
+| A packet type outside the seven in this slice, here type 2, is refused. | `Spec.rejects_unknown_type` |
 
-## What is not in this slice
+A packet is well formed when its numbers fit the widths
+that carry them, its strings obey the string rules and fit
+the two byte length prefix, its properties match the
+property table in type and place with no single use
+property repeated, its packet identifiers stand where the
+type requires them and are never 0 there, and its whole
+body is shorter than 2^28, the largest remaining length a
+variable byte integer can carry. The full list is in
+`SPEC.md`.
 
-- A broker.
-- Session state.
-- Delivery guarantees.
+The round trip theorems rest on the proofs in
+`Proofs/RoundTrip.lean`, where they are
+`Mqtt.Proofs.parsePacket_print`, `Mqtt.Proofs.parse_print`,
+and `Mqtt.Proofs.decVBI_printVBI`. All three check against
+the standard axioms only (`propext`, `Classical.choice`,
+`Quot.sound`), which a reader can confirm with
+`#print axioms`, or by running
+`lake env lean Mqtt/Verify.lean`. The refusal theorems are
+single inputs checked in the kernel with `decide +kernel`.
+Under the round trips, the field and body steps are proved
+one by one in the same file: big endian numbers, byte cuts,
+string and binary fields, typed property values, single
+properties, property lists and whole property blocks, the
+subscription options byte, topic filter lists, and the body
+of each of the seven packet types. The UTF-8 round trip,
+`Mqtt.Utf8.Proofs.decode_encode`, is proved in
+`Proofs/Utf8.lean`, and worked examples from the standard
+are proved in `Proofs/Examples.lean`.
 
-## Layout, when the first slice lands
+The command line tool in `Main.lean` calls `Mqtt.parse`
+and `Mqtt.print` directly, the same functions the theorems
+are about.
 
-The layout follows the Proven Commons template in the mission repo, under bar/template. Spec.lean holds the statements a reviewer approves. Proofs.lean holds the proofs under the same names. Main.lean holds the command line tool used by the tests. The bar check runs in CI on every change.
+## What is not proved
+
+- That the reader accepts every byte string the standard
+  allows, and rejects every one it forbids. The round trips
+  do not need either, and the refusal theorems pin single
+  inputs only, so neither holds in general as a proof. The
+  oracle differential and the mutation tests in `tests/`
+  check that behaviour instead, and the results file
+  records the outcome, including any failure.
+- The pinned reading of the variable byte integer: an
+  encoding that uses more bytes than the value needs is
+  accepted, as long as it fits in four bytes. Section
+  1.5.5 of the standard states the shortest form as a
+  requirement on senders; this reader accepts the longer
+  forms, and the printer always writes the shortest. The
+  reading is pinned in `SPEC.md`, and it is a reading, not
+  a proof.
+- Any reading of what a property means. A property is an
+  identifier and a typed value; that a Receive Maximum of
+  10 asks the peer to hold back after ten packets is broker
+  and session behaviour, and none of it is in this slice.
+- Anything about packets outside the seven types, or
+  property identifiers outside the table in `SPEC.md`.
+  Both are rejected, and that rejection is tested, apart
+  from the single inputs the refusal theorems pin.
+- Broker or session behaviour of any kind: connections,
+  subscriptions as state, retained messages, keep alive
+  timing, and what any peer does with a packet.
+- The worked examples on the printing side. The examples
+  in `Proofs/Examples.lean` are stated on the reading side,
+  because the printer's variable byte integer is defined
+  by well founded recursion, which the kernel will not
+  evaluate in a `decide` proof here. The round trip
+  theorems cover the printer.
+- Reading requests and printing answers in `Main.lean`:
+  splitting lines, and the decimal number reader. The tests
+  cover them, malformed requests included.
+- Speed. The code works on lists of bytes, which suits
+  proofs, not large packets.
+
+## What you must trust
+
+- The Lean kernel (Lean 4.35.0, pinned in
+  `lean-toolchain`), which checks every proof.
+- The Lean compiler, with the C compiler and linker
+  shipped with it, which turns the proved definitions into
+  the program that runs.
+- The Lean runtime, which runs that program.
+- The hardware the program runs on.
+- Every dependency in `lake-manifest.json`: the manifest
+  lists no packages, so there are no library dependencies
+  to trust beyond the Lean toolchain itself.
+- Lean's core library, including the compiled code it puts
+  in place of some definitions the proofs reason about.
+- The operating system the program runs on.
+- That `SPEC.md` states the reading of the MQTT 5.0
+  standard you intend. The proofs are about the reader and
+  printer in this repo following each other exactly; the
+  fidelity of the spec to the standard is a reading, pinned
+  in `SPEC.md` where the standard leaves a choice open.
+- The strict oracle in `tests/run_tests.py`, written from
+  the standard, and Paho's Python library in the parts of
+  the differential it covers. Both are evidence, not proof.
+  The results file names the versions used, and states
+  plainly which oracles were and were not available.
+- The line handling in `Main.lean` (splitting a request
+  line, reading decimal codes). The tests drive it, and no
+  proof covers it.
+- There are no exceptions to item 4 of the bar: the
+  project uses none of the features it forbids.
+
+## Re-check it
+
+1. `lake comparator --paranoid`: builds the challenge
+   file `Spec.lean` and the proofs in a sandbox and
+   checks that each theorem named in `comparator.json`
+   proves exactly the statement in the challenge file,
+   uses no axiom but the three standard ones, and is
+   accepted by Lean's kernel and every other kernel
+   shipped with Lean.
+2. `python3 tests/run_tests.py`: the fixed cases, the
+   differential against the strict oracle, the Paho
+   cross-check when the library is importable, and the
+   mutation and rejection cases, with counts and any
+   failures written to `tests/TEST-RESULTS.md`. The
+   harness uses the Paho library from the virtual
+   environment in the work directory (`venv`) when it is
+   there, and says so in the results file when it is not.
+3. `lake build`: the library, the proofs, and the tool
+   build clean, and `lake env lean Mqtt/Verify.lean`
+   prints the axiom list for the round trip theorems.
+4. Read `SPEC.md` against the MQTT 5.0 standard and check
+   the pinned readings are the ones you want.
diff --git a/SPEC.md b/SPEC.md
new file mode 100644
index 0000000..856ff19
--- /dev/null
+++ b/SPEC.md
@@ -0,0 +1,356 @@
+# MQTT packet codec: specification
+
+This is the specification of the first slice for the `mqtt`
+package: MQTT 5.0 control packet framing at the level of bytes,
+in Lean, with the round trip proved. The format itself is
+defined by the OASIS MQTT Version 5.0 standard; section numbers
+below are that standard's. This file states what the slice does
+with it, including the points where the standard leaves a
+reading open and this slice pins one.
+
+What the slice is: a reader and a printer for one control
+packet of seven types, and a reader that can walk a stream of
+packets one at a time. What it is not: a broker, a client, or
+any session behaviour. Nothing here opens a connection, keeps
+state between packets, acts on a packet's meaning, or checks a
+packet against a subscription or a session.
+
+## The packet on the wire
+
+A packet is three parts, in order:
+
+1. One fixed header byte: the packet type in the high four
+   bits, and type specific flags in the low four bits.
+2. The remaining length: a variable byte integer (below) that
+   counts the bytes of the third part.
+3. The body: the variable header and the payload for the type,
+   exactly as many bytes as the remaining length says.
+
+The packet types in this slice are CONNECT (1), PUBLISH (3),
+SUBSCRIBE (8), SUBACK (9), PINGREQ (12), PINGRESP (13), and
+DISCONNECT (14). A fixed header byte whose type nibble is any
+other value is rejected in this slice.
+
+## The variable byte integer
+
+A variable byte integer (section 2.1.4) carries seven bits per
+byte, low groups first. The top bit of a byte is a continuation
+mark: it is set on every byte but the last. At most four bytes
+are used, so the largest value is 268435455 (2^28 - 1). The
+standard's worked table:
+
+| Value | Bytes |
+| --- | --- |
+| 0 | 0 |
+| 127 | 127 |
+| 128 | 128, 1 |
+| 16383 | 255, 127 |
+| 16384 | 128, 128, 1 |
+| 2097151 | 255, 255, 127 |
+| 2097152 | 128, 128, 128, 1 |
+| 268435455 | 255, 255, 255, 127 |
+
+The reader rejects a value whose fourth byte still carries a
+continuation mark (a fifth byte would be needed), and rejects
+a value cut off by the end of the input.
+
+Pinned reading, non-minimal encodings: a value may be written
+with more bytes than it needs, as long as the writing uses at
+most four bytes and the value fits. The reader accepts such
+encodings. So 0 written as 128, 0 reads as 0. This matches the
+behaviour of common libraries, including Paho. The printer
+always writes the minimal form, so a packet that arrived with
+a non-minimal remaining length is reprinted with the minimal
+one. The same rule applies to every variable byte integer in
+a packet, including property lengths and variable byte
+integer property values.
+
+## Fixed header flags
+
+For every type in this slice except PUBLISH, the flags nibble
+must be exactly the value the standard fixes (section 2.1.2):
+0010 for SUBSCRIBE, and 0000 for CONNECT, SUBACK, PINGREQ,
+PINGRESP, and DISCONNECT. Any other nibble is rejected.
+
+PUBLISH flags carry meaning and are part of the packet value:
+the DUP flag at bit 3, the QoS level at bits 2 and 1, and the
+RETAIN flag at bit 0. The QoS value 3 is reserved and is
+rejected.
+
+## Strings and binary data
+
+A UTF-8 string field (section 1.5.4) is a two byte length,
+counting bytes, then that many bytes of UTF-8 text. The reader
+decodes the bytes with a strict UTF-8 decoder: it rejects
+stray continuation bytes, overlong forms, lead bytes above
+F4, encodings of the surrogate values D800 to DFFF, values
+above 10FFFF, and truncated sequences. It also rejects the
+null character U+0000, which the standard forbids in strings.
+Nothing else about the text is checked.
+
+A binary data field (section 1.5.3) is a two byte length, then
+that many bytes, with no check on the bytes.
+
+## Properties
+
+Most packet types carry a property block (section 2.2.2): a
+property length as a variable byte integer, then that many
+bytes of properties. Each property is an identifier, written
+as a variable byte integer, and a value whose shape is fixed
+by the identifier's row in the standard's property table
+(Table 2-4). The block must be filled exactly: a property that
+runs past the end of the block, and bytes left over inside the
+block after the last whole property, are both rejected.
+
+The table as implemented in this slice:
+
+| Id | Name | Value type | Blocks it may stand on |
+| --- | --- | --- | --- |
+| 0x01 | Payload Format Indicator | byte | will, PUBLISH |
+| 0x02 | Message Expiry Interval | four byte integer | will, PUBLISH |
+| 0x03 | Content Type | UTF-8 string | will, PUBLISH |
+| 0x08 | Response Topic | UTF-8 string | will, PUBLISH |
+| 0x09 | Correlation Data | binary data | will, PUBLISH |
+| 0x0B | Subscription Identifier | variable byte integer | PUBLISH, SUBSCRIBE |
+| 0x11 | Session Expiry Interval | four byte integer | CONNECT, DISCONNECT |
+| 0x12 | Assigned Client Identifier | UTF-8 string | none in this slice |
+| 0x13 | Server Keep Alive | two byte integer | none in this slice |
+| 0x15 | Authentication Method | UTF-8 string | CONNECT |
+| 0x16 | Authentication Data | binary data | CONNECT |
+| 0x17 | Request Problem Information | byte | CONNECT |
+| 0x18 | Will Delay Interval | four byte integer | will |
+| 0x19 | Request Response Information | byte | CONNECT |
+| 0x1A | Response Information | UTF-8 string | none in this slice |
+| 0x1C | Server Reference | UTF-8 string | DISCONNECT |
+| 0x1F | Reason String | UTF-8 string | SUBACK, DISCONNECT |
+| 0x21 | Receive Maximum | two byte integer | CONNECT |
+| 0x22 | Topic Alias Maximum | two byte integer | CONNECT |
+| 0x23 | Topic Alias | two byte integer | PUBLISH |
+| 0x24 | Maximum QoS | byte | none in this slice |
+| 0x25 | Retain Available | byte | none in this slice |
+| 0x26 | User Property | UTF-8 string pair | CONNECT, will, PUBLISH, SUBSCRIBE, SUBACK, DISCONNECT |
+| 0x27 | Maximum Packet Size | four byte integer | CONNECT |
+| 0x28 | Wildcard Subscription Available | byte | none in this slice |
+| 0x29 | Subscription Identifier Available | byte | none in this slice |
+| 0x2A | Shared Subscription Available | byte | none in this slice |
+
+Rows marked "none in this slice" name properties the standard
+assigns to packet types this slice does not read (chiefly
+CONNACK). The identifier has a known value type, but it is on
+no allowed list here, so the reader rejects it everywhere in
+this slice.
+
+Three property checks reject a packet:
+
+- An identifier with no row in the table is rejected.
+- A property standing on a block whose allowed list does not
+  include it is rejected. For example, a Subscription
+  Identifier on a CONNECT packet is rejected.
+- A repeated single use property is rejected. Two properties
+  may repeat: the User Property (0x26) may repeat on any block
+  that allows it, and the Subscription Identifier (0x0B) may
+  repeat on PUBLISH, where one message can match several
+  subscriptions (section 3.3.4). Every other allowed property
+  may stand at most once in one block.
+
+## The seven packet types
+
+### CONNECT (section 3.1)
+
+The body is: the protocol name as a string field, which must
+be exactly the text "MQTT"; one protocol level byte, which
+must be 5; one connect flags byte; the keep alive as two
+bytes; the CONNECT property block; then the payload.
+
+The connect flags byte is: username flag at bit 7, password
+flag at bit 6, will retain at bit 5, will QoS at bits 4 and 3,
+will flag at bit 2, clean start at bit 1, and a reserved bit
+at bit 0. The reader rejects a packet whose reserved bit is
+set, and rejects a will QoS field of 3. The will QoS and will
+retain bits are part of the packet value only when the will
+flag is set; when it is clear, the printer writes them as 0.
+
+The payload is: the client identifier as a string field
+(always present, and it may be empty); then, when the will
+flag is set, the will property block, the will topic as a
+string field, and the will payload as a binary data field;
+then the username as a string field when the username flag is
+set; then the password as a binary data field when the
+password flag is set. The fields stand exactly when the flags
+say they stand, and the body must be consumed exactly: bytes
+left over, or a field the flags demand but the bytes do not
+hold, are rejected. The will topic must pass the topic name
+check below, like a PUBLISH topic.
+
+### PUBLISH (section 3.3)
+
+The body is: the topic name as a string field; the packet
+identifier as two bytes, present exactly when the QoS is 1 or
+2 and never present at QoS 0; the PUBLISH property block;
+then the payload, which is all the bytes that remain in the
+body, and may be empty.
+
+The topic name must be nonempty and must contain neither
+wildcard character, `+` or `#` (section 4.7.1). A packet
+identifier, where one stands, must not be 0.
+
+### SUBSCRIBE (section 3.8)
+
+The body is: the packet identifier as two bytes, which must
+not be 0; the SUBSCRIBE property block; then a list of topic
+filters that fills the rest of the body exactly. The list
+must be nonempty. Each filter is a filter string as a string
+field, then one subscription options byte. A filter string
+follows the string rules above; wildcards are allowed in it,
+as the standard allows. The reader adds no nonemptiness check
+of its own to a single filter string.
+
+The subscription options byte is: the maximum QoS at bits 0
+and 1, the no local flag at bit 2, the retain as published
+flag at bit 3, and the retain handling choice at bits 4 and
+5. The reader rejects a byte of 64 or more (the reserved bits
+6 and 7 must be clear), a QoS field of 3, and a retain
+handling field of 3.
+
+### SUBACK (section 3.9)
+
+The body is: the packet identifier as two bytes, which must
+not be 0; the SUBACK property block; then the list of reason
+codes, one byte each, filling the rest of the body. The list
+must be nonempty. Reason code values are not checked beyond
+being bytes.
+
+### PINGREQ (section 3.12) and PINGRESP (section 3.13)
+
+Both packets have an empty body: the remaining length must be
+0, and any body byte is rejected.
+
+### DISCONNECT (section 3.14)
+
+Three body forms are legal:
+
+- A remaining length of 0: a normal disconnection with no
+  body.
+- A remaining length of 1: one reason code byte and no
+  property block. The standard omits the property length when
+  the remaining length is 1 (section 3.14.2), so this form is
+  accepted, and reads as that reason code with an empty
+  property block.
+- A remaining length of 2 or more: one reason code byte, then
+  a DISCONNECT property block that fills the rest of the body
+  exactly.
+
+The printer always writes the second kind of packet with an
+explicit property block, so a packet read from the one byte
+form is reprinted in the longer form: the packet with reason
+code 0 and no properties prints as remaining length 2, reason
+0, property length 0. Reason code values are not checked
+beyond being bytes.
+
+## The reader
+
+The reader reads one packet from the front of a byte list and
+returns the packet together with the rest of the input, so a
+caller can walk a stream of packets: trailing bytes are not
+an error at that level. The whole input form of the reader
+adds the check that nothing follows the packet.
+
+Safety: the reader never reads past the end of its input. It
+first cuts the body out by the remaining length, and each
+field reader checks its length against the bytes that
+actually remain before taking any of them. Any shortfall, at
+any point, is a rejection, not a partial read. Each type's
+reader must consume its body cut exactly.
+
+## Well formed values
+
+The round trip claim holds for well formed packets: the
+fields the printer can write exactly. In outline:
+
+- Every number fits the width that carries it: keep alive and
+  packet identifiers and two byte property values below
+  65536, four byte property values below 2^32, variable byte
+  integer values and any single property block's printed
+  length below 2^28, and the whole body below 2^28, the
+  largest remaining length four bytes can carry.
+- Strings obey the string rules and their UTF-8 byte length
+  fits the two byte length prefix; binary data fields fit the
+  same prefix.
+- Properties match the table in type and in place, and no
+  single use property repeats in one block.
+- CONNECT: the will, when one stands, has QoS at most 2, a
+  well formed will property block, a topic that passes the
+  topic name check, and a payload that fits its prefix.
+- PUBLISH: QoS at most 2; a topic that passes the topic name
+  check; a packet identifier standing exactly when the QoS is
+  1 or 2, and never 0.
+- SUBSCRIBE: a nonzero packet identifier, a nonempty filter
+  list, and options with QoS and retain handling at most 2.
+- SUBACK: a nonzero packet identifier and a nonempty reason
+  list of byte values.
+- DISCONNECT with a body: a reason code below 256 and a well
+  formed property block.
+
+## The printer
+
+The printer writes a packet as the fixed header byte, the
+remaining length as a minimal variable byte integer, and the
+body in the layouts above. Property blocks are written with a
+minimal property length. A packet read by the reader and
+printed again is in this canonical form; a packet that
+arrived already in canonical form reprints byte for byte.
+
+## The line protocol
+
+The command line tool reads one request per line: the
+operation and a payload, parted by one space. The payload is
+decimal byte numbers parted by commas, with no spaces. A
+number is plain decimal: no sign, no leading zeros (the
+number 0 itself is written `0`), at most twenty digits. An
+empty line gets no answer. A request that breaks these rules
+prints `error`, as does an unknown operation.
+
+The one operation is `parse`. It parses the bytes as exactly
+one whole packet and prints `ok:` followed by the bytes of
+the canonical reprint, comma parted, when the bytes are one
+packet this slice reads. It prints `none` when the bytes are
+well formed as a request but are not one packet this slice
+reads. The empty payload is the empty byte list and answers
+`none`.
+
+Example: the request `parse 192,0` is a PINGREQ. The answer
+is `ok:192,0`. The request `parse 224,1,0` is the one byte
+body form of DISCONNECT with reason code 0. The answer is
+`ok:224,2,0,0`: the same packet reprinted with its explicit
+property block.
+
+The tool prints only the re-encoded bytes. It does not print
+a rendering of the packet, so test harnesses check the parsed
+structure through the re-encoding together with their own
+oracle.
+
+## Properties and their theorems
+
+Each property a reader can check in the page (`README.md`)
+names its theorem. The theorems are stated in `Spec.lean`
+and proved in `Proofs/SpecProofs.lean`. The refusal theorems
+are single inputs, one for each named rejection case in the
+test harness; the tests in `tests/` cover each rule on many
+more inputs.
+
+| Property | Theorem |
+|----------|---------|
+| Parsing the printed form of a well formed packet, with more stream bytes after it, gives the packet and those bytes back | `Spec.parsePacket_print` |
+| Parsing the printed form of a well formed packet on its own gives the packet back | `Spec.parse_print` |
+| Reading a printed variable byte integer gives the number back, below 2^28 | `Spec.decVBI_printVBI` |
+| A remaining length needing a fifth byte is refused | `Spec.rejects_five_byte_remaining_length` |
+| A SUBSCRIBE with flags other than 0010 is refused | `Spec.rejects_subscribe_flags` |
+| A PUBLISH with the reserved QoS value 3 is refused | `Spec.rejects_publish_qos3` |
+| A PUBLISH topic name holding a wildcard is refused | `Spec.rejects_wildcard_topic` |
+| A CONNECT with a protocol name other than `MQTT` is refused | `Spec.rejects_wrong_protocol_name` |
+| A CONNECT with the reserved connect flag bit set is refused | `Spec.rejects_reserved_connect_flag` |
+| A property on a packet type that does not allow it is refused | `Spec.rejects_property_wrong_type` |
+| A single use property standing twice in one block is refused | `Spec.rejects_repeated_property` |
+| A SUBSCRIBE with packet identifier 0 is refused | `Spec.rejects_subscribe_id_zero` |
+| A PINGREQ with a body is refused | `Spec.rejects_pingreq_body` |
+| A packet type outside the seven in this slice is refused | `Spec.rejects_unknown_type` |
diff --git a/Spec.lean b/Spec.lean
new file mode 100644
index 0000000..b2e91c7
--- /dev/null
+++ b/Spec.lean
@@ -0,0 +1,115 @@
+/-
+  The specification as Lean statements: the challenge file.
+
+  A reviewer who did not write this file approves it, and `bar.toml`
+  records the SHA-256 it had then. The proofs live in `Proofs`
+  (`Proofs/SpecProofs.lean`); `lake comparator` checks that each one
+  proves exactly the statement written here. The `sorry` below is
+  expected in this file only.
+
+  The statements use only the definitions in `Mqtt/Value.lean`,
+  `Mqtt/Parse.lean`, and `Mqtt/Utf8.lean`, the code under proof
+  named in `bar.toml`. No definition of their own is needed, so
+  this project has no `Spec/Defs.lean`.
+-/
+
+import Mqtt
+
+open Mqtt
+
+/-! ## The round trips
+
+The statements the slice stands on. Each one is the statement of
+the proved theorem of the same shape in `Proofs/RoundTrip.lean`,
+over the same well formedness predicate, `Mqtt.PacketWF`. -/
+
+/-- Parsing the printed form of a well formed packet, with more
+    stream bytes after it, gives the packet and those bytes back.
+    So a printer that wrote nothing, or wrote something shorter,
+    fails this statement. -/
+theorem Spec.parsePacket_print (p : Packet) (rest : List UInt8)
+    (h : PacketWF p) :
+    parsePacket (print p ++ rest) = some (p, rest) := sorry
+
+/-- Parsing the printed form of a well formed packet on its own
+    gives the packet back. -/
+theorem Spec.parse_print (p : Packet) (h : PacketWF p) :
+    parse (print p) = some p := sorry
+
+/-- Reading a printed variable byte integer gives the number
+    back, for every value below 2^28, the most four bytes carry. -/
+theorem Spec.decVBI_printVBI (n : Nat) (rest : List UInt8)
+    (hn : n < 268435456) :
+    decVBI (printVBI n ++ rest) = some (n, rest) := sorry
+
+/-! ## Refused inputs
+
+Single inputs the reader refuses, one for each headline rule of
+`SPEC.md`. Each input is one of the named rejection cases in the
+test harness. The differential tests cover these rules on many
+more inputs; these statements pin them so a reader of the
+specification can check each rule against one concrete case. -/
+
+/-- A remaining length whose fourth byte carries a continuation
+    mark is refused: the value would need a fifth byte, and four
+    is the limit. -/
+theorem Spec.rejects_five_byte_remaining_length :
+    (parse ([192, 255, 255, 255, 255, 127] : List UInt8)).isSome
+      = false := sorry
+
+/-- A SUBSCRIBE packet with flags 0000 is refused: the value the
+    standard fixes for SUBSCRIBE is 0010. -/
+theorem Spec.rejects_subscribe_flags :
+    (parse ([128, 7, 0, 1, 0, 0, 1, 97, 0] : List UInt8)).isSome
+      = false := sorry
+
+/-- A PUBLISH packet with QoS 3 is refused: that QoS value is
+    reserved. -/
+theorem Spec.rejects_publish_qos3 :
+    (parse ([54, 7, 0, 1, 97, 0, 1, 0, 120] : List UInt8)).isSome
+      = false := sorry
+
+/-- A PUBLISH topic name holding a wildcard is refused: `a/#` is
+    a filter, not a topic name. -/
+theorem Spec.rejects_wildcard_topic :
+    (parse ([48, 7, 0, 3, 97, 47, 35, 0, 120] : List UInt8)).isSome
+      = false := sorry
+
+/-- A CONNECT whose protocol name is not `MQTT` is refused. -/
+theorem Spec.rejects_wrong_protocol_name :
+    (parse ([16, 14, 0, 4, 77, 81, 84, 85, 5, 2, 0, 0, 0, 0, 1, 120]
+      : List UInt8)).isSome = false := sorry
+
+/-- A CONNECT with the reserved bit of the connect flags byte
+    set is refused. -/
+theorem Spec.rejects_reserved_connect_flag :
+    (parse ([16, 14, 0, 4, 77, 81, 84, 84, 5, 3, 0, 0, 0, 0, 1, 120]
+      : List UInt8)).isSome = false := sorry
+
+/-- A property standing on a packet type that does not allow it
+    is refused: here a subscription identifier on a CONNECT. -/
+theorem Spec.rejects_property_wrong_type :
+    (parse ([16, 16, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 2, 11, 5, 0,
+      1, 120] : List UInt8)).isSome = false := sorry
+
+/-- A single use property standing twice in one block is
+    refused: here the topic alias on a PUBLISH, twice. -/
+theorem Spec.rejects_repeated_property :
+    (parse ([50, 12, 0, 1, 97, 0, 3, 6, 35, 0, 1, 35, 0, 2]
+      : List UInt8)).isSome = false := sorry
+
+/-- A SUBSCRIBE with packet identifier 0 is refused:
+    identifiers are never 0. -/
+theorem Spec.rejects_subscribe_id_zero :
+    (parse ([130, 7, 0, 0, 0, 0, 1, 97, 0] : List UInt8)).isSome
+      = false := sorry
+
+/-- A PINGREQ with a body is refused: its remaining length must
+    be 0. -/
+theorem Spec.rejects_pingreq_body :
+    (parse ([192, 1, 0] : List UInt8)).isSome = false := sorry
+
+/-- A packet type outside the seven in this slice is refused:
+    here type 2. -/
+theorem Spec.rejects_unknown_type :
+    (parse ([32, 0] : List UInt8)).isSome = false := sorry
diff --git a/bar.toml b/bar.toml
new file mode 100644
index 0000000..d1edcaa
--- /dev/null
+++ b/bar.toml
@@ -0,0 +1,67 @@
+# Read by bar/check.py in Proven-Commons/mission.
+# See playbook/verified-bar.md there for what each field means.
+
+[project]
+name = "mqtt"
+# "in-progress" until every bar item passes, then "verified".
+status = "in-progress"
+page = "README.md"
+# GitHub handles of everyone who wrote the specification.
+spec_authors = ["abu-aska"]
+# The program people run. A change to it voids the approval.
+entry_points = ["Main.lean"]
+
+[spec]
+files = ["SPEC.md", "Spec.lean"]
+# The code under proof: the functions the statements are about.
+code = [
+  # The data types the statements are about, and their constructors.
+  "Mqtt.PropType", "Mqtt.PropVal", "Mqtt.PropVal.byte",
+  "Mqtt.PropVal.twoByte", "Mqtt.PropVal.fourByte", "Mqtt.PropVal.varByte",
+  "Mqtt.PropVal.utf8", "Mqtt.PropVal.utf8Pair", "Mqtt.PropVal.binary",
+  "Mqtt.Property", "Mqtt.PropSet", "Mqtt.SubOpts", "Mqtt.Will",
+  "Mqtt.Connect", "Mqtt.Publish", "Mqtt.Packet", "Mqtt.Packet.connect",
+  "Mqtt.Packet.publish", "Mqtt.Packet.subscribe", "Mqtt.Packet.suback",
+  "Mqtt.Packet.pingreq", "Mqtt.Packet.pingresp", "Mqtt.Packet.disconnect",
+  # The property table.
+  "Mqtt.valType", "Mqtt.propTypeOf", "Mqtt.allowedOf", "Mqtt.repeatableIn",
+  # The byte forms and the printer.
+  "Mqtt.writeBE", "Mqtt.printVBI", "Mqtt.printStr", "Mqtt.printBin",
+  "Mqtt.printPropVal", "Mqtt.printProperty", "Mqtt.printPropsList",
+  "Mqtt.printProps", "Mqtt.printOptsByte", "Mqtt.connectFlags",
+  "Mqtt.printWillPart", "Mqtt.printOptStr", "Mqtt.printOptBin",
+  "Mqtt.printConnectBody", "Mqtt.publishHeader", "Mqtt.printIdOpt",
+  "Mqtt.printPublishBody", "Mqtt.printFilter", "Mqtt.printFilters",
+  "Mqtt.printSubscribeBody", "Mqtt.printSubackBody", "Mqtt.bodyOf",
+  "Mqtt.headerOf", "Mqtt.print",
+  # Well formedness.
+  "Mqtt.hasNul", "Mqtt.StrWF", "Mqtt.BinWF", "Mqtt.TopicWF", "Mqtt.ValWF",
+  "Mqtt.PropsWF", "Mqtt.PropsBlockWF", "Mqtt.WillWF", "Mqtt.ConnectWF",
+  "Mqtt.PublishWF", "Mqtt.OptsWF", "Mqtt.FiltersWF", "Mqtt.PacketFieldsWF",
+  "Mqtt.PacketWF",
+  # The strict UTF-8 codec the string reader rests on.
+  "Mqtt.Utf8.encodeChar", "Mqtt.Utf8.encode", "Mqtt.Utf8.contVal",
+  "Mqtt.Utf8.decode",
+  # The length checked readers and the parser.
+  "Mqtt.readNat", "Mqtt.readBytes", "Mqtt.readByte", "Mqtt.decVBIGo",
+  "Mqtt.decVBI", "Mqtt.checkChars", "Mqtt.readStr", "Mqtt.readBin",
+  "Mqtt.readPropVal", "Mqtt.readEntry", "Mqtt.readEntriesGo",
+  "Mqtt.readEntries", "Mqtt.readProps", "Mqtt.readOptsByte",
+  "Mqtt.readFiltersGo", "Mqtt.flagBit", "Mqtt.checkTopic",
+  "Mqtt.readWillPart", "Mqtt.readOptStrField", "Mqtt.readOptBinField",
+  "Mqtt.readConnectBody", "Mqtt.readPacketId", "Mqtt.readPublishBody",
+  "Mqtt.readSubscribeBody", "Mqtt.readSubackBody", "Mqtt.readDisconnectBody",
+  "Mqtt.parseBody", "Mqtt.parsePacket", "Mqtt.parse",
+]
+
+# One entry per approval, added in a pull request the reviewer approves.
+# [[spec.approval]]
+# reviewer = "github-handle"
+# date = "2026-11-02"
+# sha256 = "..."
+# record = "https://github.com/Proven-Commons/mqtt/pull/<n>"
+
+[tests]
+results = "tests/TEST-RESULTS.md"
+command = "python3 tests/run_tests.py"
+files = ["tests/run_tests.py"]
diff --git a/comparator.json b/comparator.json
new file mode 100644
index 0000000..72b4ed5
--- /dev/null
+++ b/comparator.json
@@ -0,0 +1 @@
+{"challenge_module":"Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Proofs","theorem_names":["Spec.parsePacket_print","Spec.parse_print","Spec.decVBI_printVBI","Spec.rejects_five_byte_remaining_length","Spec.rejects_subscribe_flags","Spec.rejects_publish_qos3","Spec.rejects_wildcard_topic","Spec.rejects_wrong_protocol_name","Spec.rejects_reserved_connect_flag","Spec.rejects_property_wrong_type","Spec.rejects_repeated_property","Spec.rejects_subscribe_id_zero","Spec.rejects_pingreq_body","Spec.rejects_unknown_type"]}
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..8cae1c0
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.3.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "mqtt",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..b5601e5
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,16 @@
+name = "mqtt"
+version = "0.1.0"
+defaultTargets = ["Mqtt", "Proofs", "mqtt"]
+
+[[lean_lib]]
+name = "Mqtt"
+
+[[lean_lib]]
+name = "Proofs"
+
+[[lean_lib]]
+name = "Spec"
+
+[[lean_exe]]
+name = "mqtt"
+root = "Main"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..a6aff06
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.35.0
diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md
new file mode 100644
index 0000000..838f533
--- /dev/null
+++ b/tests/TEST-RESULTS.md
@@ -0,0 +1,20 @@
+# Test results: mqtt
+
+Seed: 20261026. Tool: the Lean command line program, one process per section, requests batched. The harness checks parsed structure through the re-encoding the tool prints, together with its own oracle.
+
+Paho's Python library (`paho-mqtt`, version 2.1.0) was importable in the interpreter that ran this harness; the Paho cross-check ran. It covers variable byte integers and PUBLISH property blocks, the pieces the library exposes without a broker.
+
+Mosquitto was NOT present on this machine (no `mosquitto` or `mosquitto_sub` binary), so no Mosquitto tests ran.
+
+| Section | Inputs | Agreements |
+| --- | --- | --- |
+| Fixed cases (spec VBI table, one packet per type, richer hand built packets) | 30 | 30 |
+| Oracle differential, random packets of all seven types (seed 20261026) | 3000 | 3000 |
+| Paho 2.1.0 cross-check (variable byte integers and PUBLISH property blocks) | 629 | 629 |
+| Mutations and named rejections, settled by the oracle | 258 | 258 |
+| Line protocol cases | 9 | 9 |
+
+Named differences from the oracles:
+- Paho's variable byte integer decoder also accepts the non-minimal encoding 128, 0 as the value 0, matching the pinned reading in SPEC.md.
+
+Failures: none.
diff --git a/tests/run_tests.py b/tests/run_tests.py
new file mode 100644
index 0000000..c08b7e5
--- /dev/null
+++ b/tests/run_tests.py
@@ -0,0 +1,1048 @@
+#!/usr/bin/env python3
+"""Test harness for the Lean MQTT 5.0 packet codec.
+
+Layers, all settled against independent expectations:
+
+1. Fixed cases: the variable byte integer table from section
+   2.1.4 of the standard, hand built packets for each of the
+   seven packet types in this slice, and the DISCONNECT one
+   byte body form, which is legal and reprints in the longer
+   canonical form.
+
+2. A differential against a strict oracle written here from
+   the standard and from SPEC.md (including the pinned
+   readings: non-minimal variable byte integers within four
+   bytes are accepted, and the DISCONNECT body of length 1 is
+   a reason code with an empty property block): random packets
+   of all seven types with varied properties are encoded by
+   the oracle, read by the Lean tool, and the answer must be
+   the canonical reprint.
+
+3. A cross-check against Paho's Python library when it is
+   importable: its variable byte integer encoder must match
+   the oracle's, and property blocks it packs for PUBLISH are
+   read by the oracle, wrapped in packets, and fed to the Lean
+   tool. When the library is absent, the run says so and the
+   oracle carries accept and reject alone. The Mosquitto test
+   suite is a separate program, not a Python library; the run
+   checks for its binary and the results file states whether
+   it was present.
+
+Mutations of rich packets (truncation at every length, byte
+flips at every position) and a list of named rejection cases
+are settled by comparing the Lean answer with the oracle's
+answer on the same bytes.
+
+Results are written to tests/TEST-RESULTS.md. Seed 20261026.
+
+Usage: python3 tests/run_tests.py [--skip-build]
+Run it with the work directory's virtual environment
+(./venv/bin/python tests/run_tests.py) to get the Paho
+cross-check; without the library that part is skipped and
+the results file says so.
+"""
+
+import os
+import random
+import shutil
+import subprocess
+import sys
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+ROOT = os.path.dirname(HERE)
+EXE = os.path.join(ROOT, ".lake", "build", "bin", "mqtt")
+SEED = 20261026
+
+failures = []
+
+
+def check(cond, label, detail=""):
+    if not cond:
+        failures.append(f"{label}: {detail}")
+        print(f"FAIL {label}: {detail}")
+
+
+# ---------------------------------------------------------------------------
+# Batch runner: one process for many requests.
+# ---------------------------------------------------------------------------
+
+class Tool:
+    def __init__(self):
+        self.lines = []
+
+    def ask(self, line):
+        self.lines.append(line)
+        return len(self.lines) - 1
+
+    def run(self):
+        proc = subprocess.run([EXE], input="\n".join(self.lines) + "\n",
+                              capture_output=True, text=True, timeout=1200)
+        if proc.returncode != 0:
+            raise RuntimeError(f"tool exited {proc.returncode}: {proc.stderr[:500]}")
+        self.answers = proc.stdout.splitlines()
+        if len(self.answers) != len(self.lines):
+            raise RuntimeError(
+                f"answer count {len(self.answers)} != request count {len(self.lines)}")
+        return self.answers
+
+
+def req(bs):
+    return "parse " + ",".join(str(b) for b in bs)
+
+
+def want_ok(canon):
+    return "ok:" + ",".join(str(b) for b in canon)
+
+
+# ---------------------------------------------------------------------------
+# Oracle: canonical encoder and strict decoder, written from the
+# MQTT 5.0 standard and SPEC.md.
+#
+# Packet representation:
+#   ("connect", clean, keep_alive, props, client_id, will,
+#               username, password)
+#     will is None or (qos, retain, props, topic, payload bytes)
+#     username is None or str; password is None or bytes
+#   ("publish", dup, qos, retain, topic, packet_id, props, payload)
+#     packet_id is None at QoS 0
+#   ("subscribe", packet_id, props, filters)
+#     filters is a list of (str, (qos, no_local, retain_as_published,
+#                                  retain_handling))
+#   ("suback", packet_id, props, [reason, ...])
+#   ("pingreq",)  ("pingresp",)
+#   ("disconnect", None) or ("disconnect", (reason, props))
+# A property is (id, value): an int for byte, two byte, four byte,
+# and variable byte integer values; a str for a UTF-8 string value;
+# a (str, str) pair for a user property; bytes for binary data.
+# ---------------------------------------------------------------------------
+
+class Reject(Exception):
+    pass
+
+
+def enc_vbi(n):
+    out = bytearray()
+    while True:
+        d = n % 128
+        n //= 128
+        if n:
+            out.append(d + 128)
+        else:
+            out.append(d)
+            return bytes(out)
+
+
+def dec_vbi(bs, i):
+    acc = 0
+    mult = 1
+    for k in range(4):
+        if i >= len(bs):
+            raise Reject()
+        b = bs[i]
+        i += 1
+        if b < 128:
+            return acc + mult * b, i
+        if k == 3:
+            raise Reject()
+        acc += mult * (b - 128)
+        mult *= 128
+    raise Reject()
+
+
+def be16(n):
+    return n.to_bytes(2, "big")
+
+
+def dec_uint(bs, i, w):
+    if i + w > len(bs):
+        raise Reject()
+    return int.from_bytes(bs[i:i + w], "big"), i + w
+
+
+def enc_str(s):
+    raw = s.encode("utf-8")
+    return be16(len(raw)) + raw
+
+
+def dec_str(bs, i):
+    ln, i = dec_uint(bs, i, 2)
+    if i + ln > len(bs):
+        raise Reject()
+    raw = bytes(bs[i:i + ln])
+    try:
+        s = raw.decode("utf-8")
+    except UnicodeDecodeError:
+        raise Reject()
+    if "\x00" in s:
+        raise Reject()
+    return s, i + ln
+
+
+def enc_bin(b):
+    return be16(len(b)) + bytes(b)
+
+
+def dec_bin(bs, i):
+    ln, i = dec_uint(bs, i, 2)
+    if i + ln > len(bs):
+        raise Reject()
+    return bytes(bs[i:i + ln]), i + ln
+
+
+PROP_TYPE = {
+    0x01: "byte", 0x02: "four", 0x03: "utf8", 0x08: "utf8",
+    0x09: "binary", 0x0B: "var", 0x11: "four", 0x12: "utf8",
+    0x13: "two", 0x15: "utf8", 0x16: "binary", 0x17: "byte",
+    0x18: "four", 0x19: "byte", 0x1A: "utf8", 0x1C: "utf8",
+    0x1F: "utf8", 0x21: "two", 0x22: "two", 0x23: "two",
+    0x24: "byte", 0x25: "byte", 0x26: "pair", 0x27: "four",
+    0x28: "byte", 0x29: "byte", 0x2A: "byte",
+}
+
+ALLOWED = {
+    "connect": [0x11, 0x15, 0x16, 0x17, 0x19, 0x21, 0x22, 0x26, 0x27],
+    "will": [0x01, 0x02, 0x03, 0x08, 0x09, 0x18, 0x26],
+    "publish": [0x01, 0x02, 0x03, 0x08, 0x09, 0x0B, 0x23, 0x26],
+    "subscribe": [0x0B, 0x26],
+    "suback": [0x1F, 0x26],
+    "disconnect": [0x11, 0x1C, 0x1F, 0x26],
+}
+
+
+def repeatable(setname, pid):
+    return pid == 0x26 or (pid == 0x0B and setname == "publish")
+
+
+def enc_prop_val(t, v):
+    if t == "byte":
+        return bytes([v])
+    if t == "two":
+        return be16(v)
+    if t == "four":
+        return v.to_bytes(4, "big")
+    if t == "var":
+        return enc_vbi(v)
+    if t == "utf8":
+        return enc_str(v)
+    if t == "pair":
+        return enc_str(v[0]) + enc_str(v[1])
+    if t == "binary":
+        return enc_bin(v)
+    raise ValueError(t)
+
+
+def dec_prop_val(t, bs, i):
+    if t == "byte":
+        return dec_uint(bs, i, 1)
+    if t == "two":
+        return dec_uint(bs, i, 2)
+    if t == "four":
+        return dec_uint(bs, i, 4)
+    if t == "var":
+        return dec_vbi(bs, i)
+    if t == "utf8":
+        return dec_str(bs, i)
+    if t == "pair":
+        k, i = dec_str(bs, i)
+        v, i = dec_str(bs, i)
+        return (k, v), i
+    if t == "binary":
+        return dec_bin(bs, i)
+    raise ValueError(t)
+
+
+def enc_props(ps):
+    body = b"".join(enc_vbi(pid) + enc_prop_val(PROP_TYPE[pid], v)
+                    for pid, v in ps)
+    return enc_vbi(len(body)) + body
+
+
+def dec_props(setname, bs, i):
+    ln, i = dec_vbi(bs, i)
+    if i + ln > len(bs):
+        raise Reject()
+    seg = bytes(bs[i:i + ln])
+    end = i + ln
+    ps = []
+    seen = []
+    j = 0
+    while j < len(seg):
+        pid, j = dec_vbi(seg, j)
+        if pid not in PROP_TYPE or pid not in ALLOWED[setname]:
+            raise Reject()
+        if pid in seen and not repeatable(setname, pid):
+            raise Reject()
+        seen.append(pid)
+        v, j = dec_prop_val(PROP_TYPE[pid], seg, j)
+        ps.append((pid, v))
+    if j != len(seg):
+        raise Reject()
+    return ps, end
+
+
+def check_topic(s):
+    if s == "" or "+" in s or "#" in s:
+        raise Reject()
+    return s
+
+
+def flagbit(n, k):
+    return (n // (2 ** k)) % 2 == 1
+
+
+def enc_opts(o):
+    qos, no_local, rap, rh = o
+    return qos + (4 if no_local else 0) + (8 if rap else 0) + rh * 16
+
+
+def dec_opts(b):
+    if b >= 64 or b % 4 == 3 or (b // 16) % 4 == 3:
+        raise Reject()
+    return (b % 4, (b // 4) % 2 == 1, (b // 8) % 2 == 1, (b // 16) % 4)
+
+
+def enc_packet(pkt):
+    tag = pkt[0]
+    if tag == "connect":
+        _, clean, ka, props, cid, will, username, password = pkt
+        flags = ((128 if username is not None else 0)
+                 + (64 if password is not None else 0)
+                 + ((32 if will[1] else 0) + will[0] * 8 + 4
+                    if will is not None else 0)
+                 + (2 if clean else 0))
+        body = enc_str("MQTT") + bytes([5, flags]) + be16(ka)
+        body += enc_props(props)
+        body += enc_str(cid)
+        if will is not None:
+            body += enc_props(will[2]) + enc_str(will[3]) + enc_bin(will[4])
+        if username is not None:
+            body += enc_str(username)
+        if password is not None:
+            body += enc_bin(password)
+        header = 0x10
+    elif tag == "publish":
+        _, dup, qos, retain, topic, pid, props, payload = pkt
+        header = 0x30 + (8 if dup else 0) + qos * 2 + (1 if retain else 0)
+        body = enc_str(topic)
+        if pid is not None:
+            body += be16(pid)
+        body += enc_props(props) + bytes(payload)
+    elif tag == "subscribe":
+        _, pid, props, filters = pkt
+        header = 0x82
+        body = be16(pid) + enc_props(props)
+        for f, o in filters:
+            body += enc_str(f) + bytes([enc_opts(o)])
+    elif tag == "suback":
+        _, pid, props, reasons = pkt
+        header = 0x90
+        body = be16(pid) + enc_props(props) + bytes(reasons)
+    elif tag == "pingreq":
+        header, body = 0xC0, b""
+    elif tag == "pingresp":
+        header, body = 0xD0, b""
+    elif tag == "disconnect":
+        header = 0xE0
+        if pkt[1] is None:
+            body = b""
+        else:
+            body = bytes([pkt[1][0]]) + enc_props(pkt[1][1])
+    else:
+        raise ValueError(tag)
+    return bytes([header]) + enc_vbi(len(body)) + body
+
+
+def raw_packet(header, body):
+    return bytes([header]) + enc_vbi(len(body)) + bytes(body)
+
+
+def dec_connect(seg):
+    proto, i = dec_str(seg, 0)
+    if proto != "MQTT":
+        raise Reject()
+    level, i = dec_uint(seg, i, 1)
+    if level != 5:
+        raise Reject()
+    flags, i = dec_uint(seg, i, 1)
+    if flags % 2 != 0 or (flags // 8) % 4 == 3:
+        raise Reject()
+    ka, i = dec_uint(seg, i, 2)
+    props, i = dec_props("connect", seg, i)
+    cid, i = dec_str(seg, i)
+    will = None
+    if flagbit(flags, 2):
+        wprops, i = dec_props("will", seg, i)
+        wtopic, i = dec_str(seg, i)
+        check_topic(wtopic)
+        wpay, i = dec_bin(seg, i)
+        will = ((flags // 8) % 4, flagbit(flags, 5), wprops, wtopic, wpay)
+    username = None
+    if flagbit(flags, 7):
+        username, i = dec_str(seg, i)
+    password = None
+    if flagbit(flags, 6):
+        password, i = dec_bin(seg, i)
+    if i != len(seg):
+        raise Reject()
+    return ("connect", flagbit(flags, 1), ka, props, cid, will,
+            username, password)
+
+
+def dec_publish(flags, seg):
+    topic, i = dec_str(seg, 0)
+    check_topic(topic)
+    qos = (flags // 2) % 4
+    pid = None
+    if qos != 0:
+        pid, i = dec_uint(seg, i, 2)
+        if pid == 0:
+            raise Reject()
+    props, i = dec_props("publish", seg, i)
+    return ("publish", flagbit(flags, 3), qos, flagbit(flags, 0),
+            topic, pid, props, bytes(seg[i:]))
+
+
+def dec_subscribe(seg):
+    pid, i = dec_uint(seg, 0, 2)
+    if pid == 0:
+        raise Reject()
+    props, i = dec_props("subscribe", seg, i)
+    filters = []
+    while i < len(seg):
+        f, i = dec_str(seg, i)
+        if i >= len(seg):
+            raise Reject()
+        o = dec_opts(seg[i])
+        i += 1
+        filters.append((f, o))
+    if not filters:
+        raise Reject()
+    return ("subscribe", pid, props, filters)
+
+
+def dec_suback(seg):
+    pid, i = dec_uint(seg, 0, 2)
+    if pid == 0:
+        raise Reject()
+    props, i = dec_props("suback", seg, i)
+    reasons = list(seg[i:])
+    if not reasons:
+        raise Reject()
+    return ("suback", pid, props, reasons)
+
+
+def dec_disconnect(seg):
+    if len(seg) == 0:
+        return ("disconnect", None)
+    if len(seg) == 1:
+        return ("disconnect", (seg[0], []))
+    props, j = dec_props("disconnect", seg, 1)
+    if j != len(seg):
+        raise Reject()
+    return ("disconnect", (seg[0], props))
+
+
+def oracle_parse(bs):
+    """The whole input form: exactly one packet, nothing after it.
+    Returns the packet, or None when the oracle rejects."""
+    try:
+        if not bs:
+            return None
+        header = bs[0]
+        ln, i = dec_vbi(bs, 1)
+        if i + ln > len(bs):
+            return None
+        seg = bytes(bs[i:i + ln])
+        rest = i + ln
+        typ, flags = header // 16, header % 16
+        if typ == 1 and flags == 0:
+            pkt = dec_connect(seg)
+        elif typ == 3 and (flags // 2) % 4 != 3:
+            pkt = dec_publish(flags, seg)
+        elif typ == 8 and flags == 2:
+            pkt = dec_subscribe(seg)
+        elif typ == 9 and flags == 0:
+            pkt = dec_suback(seg)
+        elif typ == 12 and flags == 0 and not seg:
+            pkt = ("pingreq",)
+        elif typ == 13 and flags == 0 and not seg:
+            pkt = ("pingresp",)
+        elif typ == 14 and flags == 0:
+            pkt = dec_disconnect(seg)
+        else:
+            return None
+    except Reject:
+        return None
+    if rest != len(bs):
+        return None
+    return pkt
+
+
+def settled_answer(bs):
+    pkt = oracle_parse(bs)
+    return want_ok(enc_packet(pkt)) if pkt is not None else "none"
+
+
+# ---------------------------------------------------------------------------
+# Random packets.
+# ---------------------------------------------------------------------------
+
+TEXT = "abcdefgXYZ 019._-/"
+UNICODE = ["é", "ü", "世", "☕"]
+
+
+def rand_text(rng, lo=0, hi=10, topic_safe=False):
+    n = rng.randint(lo, hi)
+    pool = TEXT if topic_safe else TEXT + "".join(UNICODE)
+    return "".join(rng.choice(pool) for _ in range(n))
+
+
+def rand_topic(rng):
+    parts = [rand_text(rng, 1, 5, topic_safe=True)
+             for _ in range(rng.randint(1, 3))]
+    return "/".join(parts)
+
+
+def rand_filter(rng):
+    parts = []
+    for _ in range(rng.randint(1, 3)):
+        parts.append(rng.choice(["+", "#", rand_text(rng, 1, 4,
+                                                     topic_safe=True)]))
+    return "/".join(parts)
+
+
+def rand_bytes(rng, hi=12):
+    return bytes(rng.randrange(256) for _ in range(rng.randint(0, hi)))
+
+
+def rand_prop_value(rng, t):
+    if t == "byte":
+        return rng.choice([0, 1, 2, 255, rng.randrange(256)])
+    if t == "two":
+        return rng.choice([0, 1, 256, 65535, rng.randrange(65536)])
+    if t == "four":
+        return rng.choice([0, 1, 65536, 4294967295,
+                           rng.randrange(1 << 32)])
+    if t == "var":
+        return rng.choice([0, 1, 127, 128, 16383, 16384, 2097151,
+                           268435455, rng.randrange(1 << 28)])
+    if t == "utf8":
+        return rand_text(rng, 0, 8)
+    if t == "pair":
+        return (rand_text(rng, 1, 5), rand_text(rng, 0, 5))
+    if t == "binary":
+        return rand_bytes(rng, 8)
+    raise ValueError(t)
+
+
+def rand_props(rng, setname):
+    ids = list(ALLOWED[setname])
+    rng.shuffle(ids)
+    ids = ids[:rng.randint(0, min(4, len(ids)))]
+    ps = []
+    for pid in ids:
+        ps.append((pid, rand_prop_value(rng, PROP_TYPE[pid])))
+        if repeatable(setname, pid) and rng.random() < 0.4:
+            ps.append((pid, rand_prop_value(rng, PROP_TYPE[pid])))
+    return ps
+
+
+def rand_packet(rng):
+    tag = rng.choice(["connect", "publish", "publish", "subscribe",
+                      "suback", "pingreq", "pingresp", "disconnect"])
+    if tag == "connect":
+        will = None
+        if rng.random() < 0.5:
+            will = (rng.randint(0, 2), rng.random() < 0.5,
+                    rand_props(rng, "will"), rand_topic(rng),
+                    rand_bytes(rng))
+        return ("connect", rng.random() < 0.5,
+                rng.choice([0, 1, 60, 65535, rng.randrange(65536)]),
+                rand_props(rng, "connect"), rand_text(rng, 0, 8), will,
+                rand_text(rng, 1, 6) if rng.random() < 0.4 else None,
+                rand_bytes(rng) if rng.random() < 0.4 else None)
+    if tag == "publish":
+        qos = rng.choice([0, 1, 2])
+        return ("publish", rng.random() < 0.5, qos, rng.random() < 0.5,
+                rand_topic(rng),
+                rng.randint(1, 65535) if qos else None,
+                rand_props(rng, "publish"), rand_bytes(rng, 20))
+    if tag == "subscribe":
+        filters = [(rand_filter(rng),
+                    (rng.randint(0, 2), rng.random() < 0.5,
+                     rng.random() < 0.5, rng.randint(0, 2)))
+                   for _ in range(rng.randint(1, 3))]
+        return ("subscribe", rng.randint(1, 65535),
+                rand_props(rng, "subscribe"), filters)
+    if tag == "suback":
+        return ("suback", rng.randint(1, 65535),
+                rand_props(rng, "suback"),
+                [rng.choice([0, 1, 2, 128, 131, 135, 144, 161,
+                             rng.randrange(256)])
+                 for _ in range(rng.randint(1, 4))])
+    if tag == "pingreq":
+        return ("pingreq",)
+    if tag == "pingresp":
+        return ("pingresp",)
+    if rng.random() < 0.3:
+        return ("disconnect", None)
+    return ("disconnect",
+            (rng.choice([0, 4, 129, 135, 142, rng.randrange(256)]),
+             rand_props(rng, "disconnect")))
+
+
+# ---------------------------------------------------------------------------
+# Test sections.
+# ---------------------------------------------------------------------------
+
+VBI_TABLE = [
+    (0, [0]), (127, [127]), (128, [128, 1]), (16383, [255, 127]),
+    (16384, [128, 128, 1]), (2097151, [255, 255, 127]),
+    (2097152, [128, 128, 128, 1]),
+    (268435455, [255, 255, 255, 127]),
+]
+
+
+def fixed_cases():
+    tool = Tool()
+    entries = []
+
+    def add(label, bs, expected=None):
+        idx = tool.ask(req(bs))
+        entries.append((label, idx,
+                        expected if expected is not None
+                        else want_ok(bytes(bs))))
+
+    # The section 2.1.4 table, checked at the oracle first, then
+    # exercised through the tool as Subscription Identifier values
+    # on SUBSCRIBE packets, and as remaining lengths where the
+    # body size is practical.
+    for value, enc in VBI_TABLE:
+        check(list(enc_vbi(value)) == enc, f"fixed/vbi {value}",
+              "oracle encoder differs from the spec table")
+        pkt = ("subscribe", 1, [(0x0B, value)],
+               [("a", (0, False, False, 0))])
+        add(f"vbi {value} as a property value", enc_packet(pkt))
+    for value in (0, 127, 128, 16383, 16384):
+        if value == 0:
+            add("remaining length 0", bytes([192, 0]))
+        else:
+            body_len = value
+            payload = bytes(body_len - 4)
+            pkt = ("publish", False, 0, False, "a", None, [], payload)
+            bs = enc_packet(pkt)
+            check(list(bs[1:1 + len(enc_vbi(value))]) == list(enc_vbi(value)),
+                  f"fixed/remaining length {value}", "header bytes differ")
+            add(f"remaining length {value}", bs)
+    # The pinned reading: a non-minimal encoding within four bytes
+    # is accepted, and reprints in the minimal form.
+    add("vbi non-minimal 128,0 as remaining length",
+        bytes([48, 134, 0, 0, 1, 97, 0, 1, 2]),
+        want_ok(bytes([48, 6, 0, 1, 97, 0, 1, 2])))
+    add("vbi with rest in one packet stream position",
+        bytes([192, 0]), want_ok(bytes([192, 0])))
+
+    # One hand built packet per type; the literal ones are the
+    # same bytes proved in Proofs/Examples.lean.
+    add("pingreq", bytes([192, 0]))
+    add("pingresp", bytes([208, 0]))
+    add("disconnect empty", bytes([224, 0]))
+    add("disconnect reason only, canonical reprint",
+        bytes([224, 1, 0]), want_ok(bytes([224, 2, 0, 0])))
+    add("publish qos0", bytes([48, 6, 0, 1, 97, 0, 1, 2]))
+    add("publish qos1", bytes([50, 6, 0, 1, 97, 0, 1, 0]))
+    add("subscribe one filter", bytes([130, 7, 0, 1, 0, 0, 1, 97, 0]))
+    add("suback", bytes([144, 4, 0, 1, 0, 0]))
+    add("connect plain",
+        bytes([16, 14, 0, 4, 77, 81, 84, 84, 5, 2, 0, 0, 0, 0, 1, 120]))
+
+    richer = [
+        ("connect with will, username, password",
+         ("connect", True, 60,
+          [(0x11, 3600), (0x26, ("k", "v"))], "client-1",
+          (1, True, [(0x18, 30), (0x03, "text/plain")],
+           "last/will", b"\x01\x02"),
+          "user", b"secret")),
+        ("publish qos2 with properties",
+         ("publish", True, 2, True, "sensors/temp", 4242,
+          [(0x01, 1), (0x02, 600), (0x0B, 7), (0x0B, 9),
+           (0x26, ("a", "b")), (0x23, 3)], b"hello")),
+        ("subscribe two filters",
+         ("subscribe", 9, [(0x0B, 12)],
+          [("sensors/+", (1, True, False, 1)),
+           ("alerts/#", (2, False, True, 2))])),
+        ("suback with reason string",
+         ("suback", 9, [(0x1F, "done")], [0, 1, 128])),
+        ("disconnect with properties",
+         ("disconnect", (142, [(0x11, 0), (0x1F, "bye")]))),
+        ("disconnect reason with empty properties",
+         ("disconnect", (0, []))),
+    ]
+    for label, pkt in richer:
+        bs = enc_packet(pkt)
+        check(oracle_parse(bs) == pkt, f"fixed/{label}",
+              "oracle does not read its own packet back")
+        add(label, bs)
+
+    answers = tool.run()
+    for label, idx, expected in entries:
+        check(answers[idx] == expected, f"fixed/{label}",
+              f"got {answers[idx]}, want {expected}")
+    return len(entries)
+
+
+def oracle_differential(rng, count):
+    tool = Tool()
+    entries = []
+    for _ in range(count):
+        pkt = rand_packet(rng)
+        bs = enc_packet(pkt)
+        idx = tool.ask(req(bs))
+        entries.append((idx, want_ok(bs), pkt[0]))
+    answers = tool.run()
+    agree = 0
+    seen_types = set()
+    for idx, expected, tag in entries:
+        seen_types.add(tag)
+        if answers[idx] == expected:
+            agree += 1
+        else:
+            check(False, "oracle differential",
+                  f"got {answers[idx]}, want {expected}")
+    check(seen_types == {"connect", "publish", "subscribe", "suback",
+                         "pingreq", "pingresp", "disconnect"},
+          "oracle differential coverage", f"types seen: {seen_types}")
+    return len(entries), agree
+
+
+def paho_section(rng, count_props):
+    """Cross-checks against Paho: variable byte integers, and
+    PUBLISH property blocks packed by the library. Returns
+    (inputs, agreements)."""
+    from paho.mqtt.properties import Properties, VariableByteIntegers
+    from paho.mqtt.packettypes import PacketTypes
+    tool = Tool()
+    entries = []
+    total = 0
+    agree = 0
+    block_agree = 0
+
+    values = [v for v, _ in VBI_TABLE]
+    values += [rng.randrange(1 << 28) for _ in range(120)]
+    for v in values:
+        total += 1
+        if bytes(VariableByteIntegers.encode(v)) == enc_vbi(v):
+            agree += 1
+        else:
+            check(False, "paho vbi", f"encode {v} differs")
+    total += 1
+    if VariableByteIntegers.decode(bytes([128, 0])) == (0, 2):
+        agree += 1
+    else:
+        check(False, "paho vbi", "non-minimal decode differs")
+
+    attr = {0x01: "PayloadFormatIndicator", 0x02: "MessageExpiryInterval",
+            0x03: "ContentType", 0x08: "ResponseTopic",
+            0x09: "CorrelationData", 0x0B: "SubscriptionIdentifier",
+            0x23: "TopicAlias", 0x26: "UserProperty"}
+    for _ in range(count_props):
+        props = Properties(PacketTypes.PUBLISH)
+        chosen = []
+        if rng.random() < 0.7:
+            props.PayloadFormatIndicator = rng.randint(0, 1)
+        if rng.random() < 0.5:
+            props.MessageExpiryInterval = rng.randrange(1 << 32)
+        if rng.random() < 0.5:
+            props.ContentType = rand_text(rng, 1, 6, topic_safe=True)
+        if rng.random() < 0.4:
+            props.ResponseTopic = rand_topic(rng)
+        if rng.random() < 0.4:
+            props.CorrelationData = rand_bytes(rng, 6)
+        if rng.random() < 0.5:
+            props.SubscriptionIdentifier = [rng.randint(1, 1000)
+                                            for _ in range(rng.randint(1, 2))]
+        if rng.random() < 0.5:
+            props.TopicAlias = rng.randint(1, 65535)
+        if rng.random() < 0.5:
+            props.UserProperty = [(rand_text(rng, 1, 4, topic_safe=True),
+                                   rand_text(rng, 0, 4, topic_safe=True))]
+        packed = bytes(props.pack())
+        try:
+            parsed, j = dec_props("publish", packed, 0)
+            okshape = j == len(packed)
+        except Reject:
+            okshape = False
+        total += 1
+        if not okshape or enc_props(parsed) != packed:
+            check(False, "paho properties",
+                  f"oracle cannot read paho block {list(packed)}")
+            continue
+        block_agree += 1
+        pkt = ("publish", False, 1, False, "paho/topic", 7, parsed,
+               b"\x10\x20")
+        bs = enc_packet(pkt)
+        idx = tool.ask(req(bs))
+        entries.append((idx, want_ok(bs)))
+        total += 1
+    answers = tool.run()
+    packet_agree = 0
+    for idx, expected in entries:
+        if answers[idx] == expected:
+            packet_agree += 1
+        else:
+            check(False, "paho packet",
+                  f"got {answers[idx]}, want {expected}")
+    agree += block_agree + packet_agree
+    return total, agree
+
+
+def mutation_cases(rng):
+    tool = Tool()
+    entries = []
+
+    def settle(label, bs):
+        idx = tool.ask(req(bs))
+        entries.append((label, idx, settled_answer(bs)))
+
+    def expect(label, bs, expected):
+        idx = tool.ask(req(bs))
+        entries.append((label, idx, expected))
+        check(settled_answer(bs) == expected, f"mutation/{label}",
+              "oracle disagrees with the named expectation")
+
+    rich_connect = enc_packet(
+        ("connect", True, 60, [(0x11, 3600), (0x26, ("k", "v"))],
+         "client-1",
+         (1, True, [(0x18, 30)], "last/will", b"\x01\x02"),
+         "user", b"secret"))
+    rich_publish = enc_packet(
+        ("publish", False, 1, False, "sensors/temp", 4242,
+         [(0x02, 600), (0x26, ("a", "b"))], b"hello world"))
+    for name, base in (("connect", rich_connect),
+                       ("publish", rich_publish)):
+        for cut in range(len(base)):
+            settle(f"{name} truncate {cut}", base[:cut])
+        for off in range(len(base)):
+            mut = bytearray(base)
+            mut[off] = (mut[off] + 37) % 256
+            settle(f"{name} flip at {off}", bytes(mut))
+
+    def props_packet(setname_header, body_props, tail):
+        return raw_packet(setname_header, body_props + tail)
+
+    named = []
+    # Five byte remaining length: a continuation mark on the
+    # fourth byte.
+    named.append(("five byte remaining length",
+                  bytes([192, 255, 255, 255, 255, 127]), "none"))
+    named.append(("remaining length larger than input",
+                  bytes([192, 5, 0]), "none"))
+    named.append(("remaining length larger than a publish body",
+                  bytes([48, 100, 0, 1, 97]), "none"))
+    named.append(("truncated connect variable header",
+                  bytes([16, 8, 0, 4, 77, 81, 84, 84, 5]), "none"))
+    named.append(("wrong flags on connect", bytes([17, 0]), "none"))
+    named.append(("wrong flags on suback",
+                  bytes([146, 4, 0, 1, 0, 0]), "none"))
+    named.append(("wrong flags on pingreq", bytes([193, 0]), "none"))
+    sub_body = be16(1) + b"\x00" + enc_str("a") + b"\x00"
+    named.append(("subscribe with flags 0000",
+                  raw_packet(0x80, sub_body), "none"))
+    pub_body = enc_str("a") + be16(1) + b"\x00" + b"x"
+    named.append(("publish qos 3", raw_packet(0x36, pub_body), "none"))
+    wild_body = enc_str("a/#") + b"\x00" + b"x"
+    named.append(("publish wildcard topic",
+                  raw_packet(0x30, wild_body), "none"))
+    badname = (enc_str("MQTU") + bytes([5, 2]) + be16(0) + b"\x00"
+               + enc_str("x"))
+    named.append(("connect wrong protocol name",
+                  raw_packet(0x10, badname), "none"))
+    reserved = bytearray(rich_connect)
+    # The connect flags byte: header(1) + length(1) + name(6)
+    # + level(1) puts it at index 9.
+    reserved[9] = reserved[9] | 1
+    named.append(("connect reserved flag bit", bytes(reserved), "none"))
+    willqos = (enc_str("MQTT") + bytes([5, 2 | 4 | 24]) + be16(0)
+               + b"\x00" + enc_str("x") + b"\x00" + enc_str("w")
+               + enc_bin(b""))
+    named.append(("connect will qos 3", raw_packet(0x10, willqos), "none"))
+    wrong_prop = (enc_str("MQTT") + bytes([5, 2]) + be16(0)
+                  + enc_props([(0x0B, 5)]) + enc_str("x"))
+    named.append(("subscription identifier on connect",
+                  raw_packet(0x10, wrong_prop), "none"))
+    table_only = raw_packet(0xE0, bytes([0]) + enc_props([(0x12, "x")]))
+    named.append(("assigned client identifier on disconnect",
+                  table_only, "none"))
+    unknown_prop = raw_packet(
+        0x30, enc_str("a") + b"\x04\x7f\x01\x00\x00" + b"")
+    named.append(("unknown property identifier", unknown_prop, "none"))
+    repeated = raw_packet(
+        0x32, enc_str("a") + be16(3) + enc_props([(0x23, 1), (0x23, 2)]))
+    named.append(("repeated single use property", repeated, "none"))
+    overrun = raw_packet(0x30, enc_str("a") + b"\x0a\x01\x01")
+    named.append(("property block length overruns", overrun, "none"))
+    named.append(("packet identifier 0 in subscribe",
+                  raw_packet(0x82, be16(0) + b"\x00" + enc_str("a")
+                             + b"\x00"), "none"))
+    named.append(("packet identifier 0 in publish qos1",
+                  raw_packet(0x32, enc_str("a") + be16(0) + b"\x00"),
+                  "none"))
+    named.append(("empty topic filter list",
+                  raw_packet(0x82, be16(1) + b"\x00"), "none"))
+    named.append(("empty reason list in suback",
+                  raw_packet(0x90, be16(1) + b"\x00"), "none"))
+    named.append(("disconnect body of length 1, accepted",
+                  bytes([224, 1, 0]), want_ok(bytes([224, 2, 0, 0]))))
+    named.append(("pingreq with a body", bytes([192, 1, 0]), "none"))
+    named.append(("packet type 2, outside this slice",
+                  bytes([32, 0]), "none"))
+    named.append(("packet type 0", bytes([0, 0]), "none"))
+    named.append(("trailing byte after one packet",
+                  bytes([192, 0, 0]), "none"))
+    named.append(("empty input", b"", "none"))
+    nul_topic = raw_packet(0x30, be16(2) + b"a\x00" + b"\x00")
+    named.append(("null character in publish topic", nul_topic, "none"))
+    bad_utf8 = raw_packet(0x30, be16(1) + b"\xff" + b"\x00")
+    named.append(("ill formed utf-8 in publish topic", bad_utf8, "none"))
+    overlong = raw_packet(0x30, be16(2) + b"\xc0\x80" + b"\x00")
+    named.append(("overlong utf-8 in publish topic", overlong, "none"))
+    for opts_byte, label in ((64, "options byte reserved bits set"),
+                             (3, "options byte qos 3"),
+                             (48, "options byte retain handling 3")):
+        named.append((label,
+                      raw_packet(0x82, be16(1) + b"\x00" + enc_str("a")
+                                 + bytes([opts_byte])), "none"))
+    for label, bs, expected in named:
+        expect(label, bs, expected)
+    answers = tool.run()
+    agree = 0
+    for label, idx, expected in entries:
+        if answers[idx] == expected:
+            agree += 1
+        else:
+            check(False, f"mutation/{label}",
+                  f"got {answers[idx]}, want {expected}")
+    return len(entries), agree
+
+
+def protocol_cases():
+    lines = ["parse 192,0", "parse", "parse 01", "parse 256",
+             "parse 192,0,0", "bogus 1", "parse 1 2", "Parse 192,0",
+             "parse 0", ""]
+    expected = ["ok:192,0", "none", "error", "error", "none",
+                "error", "error", "error", "none"]
+    proc = subprocess.run([EXE], input="\n".join(lines) + "\n",
+                          capture_output=True, text=True, timeout=120)
+    got = proc.stdout.splitlines()
+    check(got == expected, "protocol", f"got {got}, want {expected}")
+    return len(expected)
+
+
+# ---------------------------------------------------------------------------
+
+def main():
+    if "--skip-build" not in sys.argv:
+        subprocess.run(["lake", "build"], cwd=ROOT, check=True,
+                       capture_output=True, text=True, timeout=1200)
+    rng = random.Random(SEED)
+    sections = []
+
+    n_fixed = fixed_cases()
+    sections.append(("Fixed cases (spec VBI table, one packet per type, "
+                     "richer hand built packets)", n_fixed, n_fixed))
+
+    n_or, a_or = oracle_differential(rng, 3000)
+    sections.append(("Oracle differential, random packets of all seven "
+                     "types (seed 20261026)", n_or, a_or))
+
+    try:
+        import paho.mqtt
+        import importlib.metadata as md
+        try:
+            paho_version = md.version("paho-mqtt")
+        except Exception:
+            paho_version = "unknown"
+        paho_present = True
+    except ImportError:
+        paho_present = False
+        paho_version = None
+    named = []
+    if paho_present:
+        n_pa, a_pa = paho_section(rng, 250)
+        sections.append((f"Paho {paho_version} cross-check (variable byte "
+                         "integers and PUBLISH property blocks)",
+                         n_pa, a_pa))
+        named.append("Paho's variable byte integer decoder also accepts "
+                     "the non-minimal encoding 128, 0 as the value 0, "
+                     "matching the pinned reading in SPEC.md.")
+
+    n_mut, a_mut = mutation_cases(rng)
+    sections.append(("Mutations and named rejections, settled by the "
+                     "oracle", n_mut, a_mut))
+    n_proto = protocol_cases()
+    sections.append(("Line protocol cases", n_proto, n_proto))
+
+    mosquitto = shutil.which("mosquitto") or shutil.which("mosquitto_sub")
+    failed = len(failures)
+    lines = []
+    lines.append("# Test results: mqtt")
+    lines.append("")
+    lines.append(f"Seed: {SEED}. Tool: the Lean command line program, "
+                 "one process per section, requests batched. The harness "
+                 "checks parsed structure through the re-encoding the "
+                 "tool prints, together with its own oracle.")
+    lines.append("")
+    if paho_present:
+        lines.append(f"Paho's Python library (`paho-mqtt`, version "
+                     f"{paho_version}) was importable in the interpreter "
+                     "that ran this harness; the Paho cross-check ran. "
+                     "It covers variable byte integers and PUBLISH "
+                     "property blocks, the pieces the library exposes "
+                     "without a broker.")
+    else:
+        lines.append("Paho's Python library (`paho-mqtt`) was NOT "
+                     "importable in the interpreter that ran this "
+                     "harness; the Paho cross-check did not run, and "
+                     "the strict oracle carried accept and reject "
+                     "alone.")
+    lines.append("")
+    if mosquitto:
+        lines.append(f"A Mosquitto binary was found at {mosquitto}; "
+                     "no Mosquitto test cases are wired into this "
+                     "harness.")
+    else:
+        lines.append("Mosquitto was NOT present on this machine (no "
+                     "`mosquitto` or `mosquitto_sub` binary), so no "
+                     "Mosquitto tests ran.")
+    lines.append("")
+    lines.append("| Section | Inputs | Agreements |")
+    lines.append("| --- | --- | --- |")
+    for name, total, agree in sections:
+        lines.append(f"| {name} | {total} | {agree} |")
+    lines.append("")
+    if named:
+        lines.append("Named differences from the oracles:")
+        for d in named:
+            lines.append(f"- {d}")
+    else:
+        lines.append("Named differences from the oracles: none.")
+    lines.append("")
+    if failed:
+        lines.append(f"Failures: {failed}.")
+        for f in failures[:40]:
+            lines.append(f"- {f}")
+    else:
+        lines.append("Failures: none.")
+    lines.append("")
+    with open(os.path.join(HERE, "TEST-RESULTS.md"), "w") as fh:
+        fh.write("\n".join(lines))
+    total = sum(t for _, t, _ in sections)
+    agree = sum(a for _, _, a in sections)
+    print(f"sections={len(sections)} inputs={total} agreements={agree} "
+          f"failures={failed} paho={'yes ' + str(paho_version) if paho_present else 'no'} "
+          f"mosquitto={'yes' if mosquitto else 'no'}")
+    return 1 if failed else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())